Post-Doctoral Research Visit F/M Bridging the gap between combinatorial proof theory and subatomic proof theory
Contract type : Fixed-term contract
Level of qualifications required : PhD or equivalent
Fonction : Post-Doctoral Research Visit
About the research centre or Inria department
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 since 2021.
The centre has 39 project teams , 27 of which operate jointly with Paris-Saclay University and the Institut Polytechnique de Paris. Its activities occupy over 600 scientists and research and innovation support staff, including 54 different nationalities.
Context
The PARTOUT team is based at the Inria research center Saclay which located at the heart of the Paris-Saclay scientific and technological excellence cluster. It is closely connected to the Université Paris-Saclay and the Institut Polytechnique de Paris, and it has over 600 scientists working in 37 project teams.
In 2019, Inria and University College London (UCL) signed an agreement to strengthen and structure the impact of scientific collaborations between the Institute and its London partners, first and foremost UCL, particularly in the fields of artificial intelligence, machine learning and statistics, as well as all scientific fields of interest to Inria.
Assignment
Candidates for postdoctoral positions are recruited after the end of their Ph.D. or after a first post-doctoral period: for the candidates who obtained their PhD in the Northern hemisphere, the date of the Ph.D. defense shall be later than September 1, 2022; in the Southern hemisphere, later than April 1, 2022. 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.
Main activities
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.
Skills
Fluent in English. Knowledge of French is not a requirement for the position. There are French courses available on-site, if you are interested.
Benefits package
- 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
Remuneration
2788 € gross/month
General Information
- Theme/Domain : Proofs and Verification
- Town/city : Palaiseau
- Inria Center : Centre Inria de Saclay
- Starting date : 2025-11-01
- Duration of contract : 2 years
- Deadline to apply : 2025-10-31
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Contacts
- Inria Team : PARTOUT (DRI)
-
Recruiter :
Strassburger Lutz / Lutz.Strassburger@inria.fr
The keys to success
The successful candidate should have profound expertise in all areas of proof theory. A thesis in an area related to deep inference would be a real asset. Some background in combinatorics would also be helpful.
About Inria
Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.