# PhD Informatics Studentship: Categorical Semantics of Deep Inference Formalisms

### University of Sussex

Qualification Type: PhD Sussex, Falmer UK Students, EU Students, International Students £18,662 per year Full Time
Placed On: 23rd November 2023 15th January 2024

Location: Brighton

Funding description: 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.

A 3.5 year PhD studentship in the department of Informatics under the supervision of Dr Alessio Santamaria. Available for April and September 2024 entry.

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.

How to apply

Apply via the postgraduate application system for a full time PhD in Informatics.

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.

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.

Type / Role:

Subject Area(s):

Location(s):

#### jobs.ac.uk Account Required

In order to create multiple alerts, you must create a jobs.ac.uk jobseeker account

#### Creation Failed

When you create this PhD alert we will email you a selection of PhDs matching your criteria.When you create this job alert we will email you a selection of jobs matching your criteria. Our Terms and Conditions and Privacy Policy apply to this service. Any personal data you provide in setting up this alert is processed in accordance with our Privacy Notice