Proof theory is a central area of theoretical computer science, as it
can provide the foundations not only for logic programming and
functional programming, but also for the formal verification of
software. Yet, despite the crucial role played by formal proofs, we
have no proper notion of proof identity telling us when two proofs are
``the same''. This is very different from other areas of mathematics,
like group theory, where two groups are ``the same'' if they
are isomorphic, or topology, where two spaces are ``the same'' if they are
homeomorphic.
The problem is that proofs are usually presented by syntactic means,
and depending on the chosen syntactic formalism, ``the same'' proof
can look very different. This is the motivation to find ways to
describe proofs independent of the formalisms, i.e.,
``canonical representations'' which do not rely on some particular
syntax of a chosen deductive formalism. One such presentation
is given by combinatorial proofs which represent proofs as
graphs that abstract away from the syntax of the proof rules.
Subatomic proof theory takes the opposite approach. It treats
atoms like binary connectives. This unifies the rules of inference to
a single shape, but it also introduces more syntax. This additional
syntax is helpful for studying various forms of proof normalizations,
but it is in the way for studying proof identity.
The work of the successful postdoc candidate will focus on investigating ways to combine the advantages of combinatorial proofs and subatomic proofs. For this the postdoc will profit from the expertise of the PARTOUT team in all areas of proof theory, in particular, in the area of the deep deep inference formalism, which has close connections with combinatorial proof theory and subatomic proof theory.
