[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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:[email protected].
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.
