Post-Doctoral Research Visit F/M [DRI Campaign] Proof Representations: Linear and Fixed-Point Decompositions of Logical Modalities

Télécharger l'offre au format PDF
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

Contexte et atouts du poste

Every year Inria International Relations Department has a few postdoctoral positions in order to support Inria international collaborations. This postdoctoral offer will be in collaboration with UCL (University College in London), UK, being jointly supervised by Elaine Pimentel (UCL) and Alexis Saurin (INRIA Paris, Picube team).

The postdoctoral contract will have a duration of 12 to 24 months. The expected start date is November 1st, 2025 and not later than January, 1st 2026. The postdoctoral fellow will be recruited by the Inria Centre of Paris, France, within the Picube team, with potential research stays at UCL, Lonon. (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

The recruited person, supervised by Elaine Pimentel (UCL) and Alexis Saurin (Picube team) is expected to conduct research on proof representations, using linear logic and fixed-point logic to design decompositions of logical modalities; this research will span :

1) from pure proof-theoretical research, aiming at understanding how linear logic an the mu-calculus can be used to decompose a variety of modal logics, aiming at providing a uniform account of those various logics, factoring structuring theorems through the properties of the encodings and providing a study of ecumenical proof systems with fixed-points;

2) to computational interpretation of logics, by developing cut-reduction systems for various systems adapted from Kozen's mu-calculus;

3) via the mechanization of the meta-theory of the above proof-theory in the Coq/Rocq proof assistant. 

For more information on the proposed research subject :
A state of the art, bibliography and scientific references are available at the following URL: https://www.irif.fr/_media/users/saurin/misc/post_doc_inria_ucl.pdf. 

 

Principales activités

  • Develop research in computational logic and proof-theory;
  • Participate to Picube team activities (in particular seminars at Picube, IRIF lab and INRIA Paris);
  • Contribute to a multi-site Paris-London collaboration;
  • Contribute to writing scientific papers for peer-reviewed publications;
  • Present the results in seminars and scientific conferences;
  • Contributed to a Coq / Rocq library

Compétences

Required:

  • PhD in Logic, Theoretical Computer Science or Mathematics.
  • Demonstrated research experience in one or more of: proof theory, interactive proof assistants, proof-as-program correspondence, modal logic, fixed-point logic.
  • Good communication skills

Preferred: 

  • Experience with proof assistants

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 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