PhD Informatics Studentship: Categorical Semantics of Deep Inference Formalisms (2024)

What you get

For 3.5 years, you will receive a tax-free stipend at a standard rate of £18,662 per year and your fees will be waived (at the UK, EU, or International rate). In addition, to a one-off Research and Training Support Grant of £2,000.

Type of award

Postgraduate Research

PhD project

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 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 http://alessio.guglielmi.name/res/cos/ .

Eligibility

The stipend is available to: UK / EU / Overseas.

The fee waiver is available to: UK / EU / Overseas.

Eligible candidates will have an upper second-class (2:1) undergraduate degree or above, in Computer Science or Mathematics and a strong interest in logic and/or category theory.

Number of scholarships available

1

Deadline

15 January 2024 23:45

How to apply

Apply via the postgraduate application system for a full time PhD in Informatics.
Please upload a personal statement detailing your research interests ans background, a copy of your degree transcripts and certificates, English-language test (if required) and two academic references.

For guidance on the application process, please see here.

Please clearly state on your application form that you are applying for the Categorical Semantics of Deep Inference formalisms studentship, under the supervision of Dr Alessio Santamaria. 

Contact us

For project specific enquiries, please email Dr Alessio Santamaria: a.santamaria@sussex.ac.uk.

For general application enquiries, please email phd.informatics@sussex.ac.uk.