Post-Doctoral Research Visit F/M Bridging the gap between combinatorial proof theory and subatomic proof theory
Type de contrat : CDD
Contrat renouvelable : Oui
Niveau de diplôme exigé : Thèse ou équivalent
Fonction : Post-Doctorant
Niveau d'expérience souhaité : Jeune diplômé
Contexte et atouts du poste
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 12 to 24 months. The default start date is November 1st, 2024
and not later than January 1st, 2025. 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)
Mission confiée
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.
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.
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.
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
Informations générales
- Thème/Domaine :
Preuves et vérification
Ingénierie logicielle (BAP E) - Ville : Palaiseau
- Centre Inria : Centre Inria de Saclay
- Date de prise de fonction souhaitée : 2024-11-01
- Durée de contrat : 12 mois
- Date limite pour postuler : 2024-06-30
Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.
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
-
Recruteur :
Strassburger Lutz / Lutz.Strassburger@inria.fr
L'essentiel pour réussir
The successful candidate should have a strong background in proof theory and/or combinatorics. Knowledge in proof complexity would be a plus.
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’institut fait appel à de nombreux talents dans plus d’une quarantaine de métiers différents. 900 personnels d’appui à la recherche et à l’innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.