Post-Doctoral Research Visit F/M Bridging the gap between combinatorial proof theory and subatomic proof theory

The Inria Saclay-Île-de-France Research Centre was established in 2008. It has developed as part of the Saclay site in partnership with Paris-Saclay University and with the Institut Polytechnique de Paris .

The centre has 40 project teams , 27 of which operate jointly with Paris-Saclay University and the Institut Polytechnique de Paris; Its activities occupy over 600 people, scientists and research and innovation support staff, including 44 different nationalities.

Every year Inria International Relations Department has a few postdoctoral positions in order to support Inria international collaborations.

The postdoctoral contract will have a duration of {\bf 12 to 24 months}. The default start date is November~1st,~2026 and not later than January 1st, 2027. The postdoctoral fellow will be recruited by the Inria Saclay Research Centre in France but it is recommended that the time is shared between France and the UK (please note that the postdoctoral fellow has to start his/her contract being in France and that the visits have to respect Inria rules for missions.

Candidates for postdoctoral positions are recruited after the end of their Ph.D. or after a first post-doctoral period: To be eligible, candidates must have defended their Ph.D. no more than 3 years before the start date of the contract. As the start date will be between November 1, 2026 and January 1, 2027, the latest eligible Ph.D. defense date will vary accordingly (approximately between November 1, 2023 and January 1, 2024).

In order to encourage mobility, the postdoctoral position must take place in a scientific environment that is truly different from the one of the Ph.D. (and, if applicable, from the position held since the Ph.D.); particular attention is thus paid to French or international candidates who obtained their doctorate abroad.

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.

Main activities (5 maximum) : do research, write papers

Additional activities (3 maximum) : teaching

The successful candidate should have a strong background in proof theory and/or combinatorics. Knowledge in proof complexity would be a plus.

• Subsidized meals
• Partial reimbursement of public transport costs
• Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
• Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
• Professional equipment available (videoconferencing, loan of computer equipment, etc.)
• Social, cultural and sports events and activities
• Access to vocational training
• Social security coverage

Monthly gross salary 2.788 euros