[TYPES/announce] Fully funded PhD position in categorical semantics

[Alessio Santamaria]

Dear all,

I have a fully funded 3.5-year PhD position in logic and category theory available at the Department of Informatics of the University of Sussex, UK. Below is a possible project proposal, however I'm open to discussion and I'd be very happy to adapt it to any candidate with a strong interest in logic and category theory, as well as to consider self-proposed projects in these areas.

The position comes with tax-free stipend at a standard rate of £18,662 per year and fees will be waived (at the UK, EU, or international rate) for 3.5 years. In addition, the student will have available a one-off Research and Training Support Grant of £2,000. 

The student will join the Foundations of Software System group at Sussex, which is fast growing (three new lecturers are joining us this academic year) and comprises researchers in logic, type theory, semantics of programming languages, formal verification, quantum theory, term rewriting, category theory, and network systems. The university campus is not far from the city of Brighton, with excellent quality of life (it's by the sea) and direct connections to Gatwick Airport and London. 
For any information about the position and how to apply, please email me at mailto:a.santamaria at sussex.ac.uk. 

With kind regards,
Alessio Santamaria

---
Proposed project title: Categorical semantics of Deep Inference formalisms.

Deep Inference is a methodology for designing formal proof systems that generalise Gentzen's formalisms of sequent calculus and natural deduction. In a Deep Inference formalism one is allowed to apply logical rules to connectives that are arbitrarily deep inside a formula, instead of just the main connective, hence the name "deep inference". From this simple concept stem several consequences, here are a few:

1. Proofs can be composed using the same connectives that build up the formulae.
2. Structural rules can be reduced, without loss of information, to an atomic form.
3. We can extract from a proof a graph, called "atomic flow", which discards the connectives and only keeps track of the atoms, from their creation to their destruction.

The compositional nature of deep inference proofs makes category theory a natural setting for an algebraic semantics of these proofs. In particular, atomic flows are reminiscent of string diagrams for monoidal categories. Another operation for deep inference proofs that is being currently developed is substitution of proofs into others, as a generalisation of the usual notion of substitution of a formula inside the atom occurrences of another. From the categorical point of view, in very simple cases, this looks like horizontal composition of natural and extranatural transformations. For more details about deep inference, see https://urldefense.com/v3/__http://alessio.guglielmi.name/res/cos/__;!!IBzWLUs!UmBnnxaGD1UiK9Pyto-HC6bUZ4yTcfbNodk2KIR0jPHvxGHB6pIRxn0gDu302nC-TbDzBaHQTtd6sNWNYvZ1tTqp59PvHu3FBO7BVjMsQg$  .
This project aims to giving a precise, sound and complete categorical semantics to deep inference formalisms of various logics with substitution. The PhD student will need to have a 2:1 degree or equivalent in Computer Science or Mathematics and a strong interest in logic and/or category theory.