Post-doctoral Research Visit F/m Bridging The Gap Between Combinatorial Proof Theory and Subatomic Proof Theory

Le descriptif de l’offre ci-dessous est en Anglais_

**Type de contrat**: CDD

**Niveau de diplôme exigé**: Thèse ou équivalent

**Fonction**: Post-Doctorant

**A propos du centre ou de la direction fonctionnelle**:
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.

**Contexte et atouts du poste**:
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.

**Mission confiée**:
**Principales activités**:
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.

**Compétences**:
Fluent in English. Knowledge of French is not a requirement for the position. There are French courses available on-site, if you are interested.

**Avantages**:

- 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

**Rémunération**:
2788 € gross/month

**Informations générales**:

- **Thème/Domaine**: Preuves et vérification
- **Ville**: Palaiseau
- **Centre Inria**: Centre Inria de Saclay
- **Date de prise de fonction souhaitée**: 2025-11-01
- **Durée de contrat**: 2 ans
- **Date limite pour postuler**: 2025-10-31

**Consignes pour postuler**:
**Sécurité défense**:
Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.

**Politique de recrutement**:
Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.

**Contacts**:

- **Équipe Inria**: PARTOUT (DRI)
- **Recruteur**:
**L'essentiel pour réussir**:
**A propos d'Inria**:
Inria est l’institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l’interface d’autres disciplines. L’i