Post-Doctoral Research Visit F/M [DRI Campaign] Proof Representations: Linear and Fixed-Point Decompositions of Logical Modalities
Contract type : Fixed-term contract
Level of qualifications required : PhD or equivalent
Fonction : Post-Doctoral Research Visit
Context
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).
Assignment
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.
Main activities
- 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
Skills
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
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 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
General Information
- Theme/Domain : Proofs and Verification
- Town/city : Paris
- Inria Center : Centre Inria de Paris
- Starting date : 2025-11-01
- Duration of contract : 2 years
- Deadline to apply : 2025-06-01
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
Eligibility criteria:
Candidates for postdoctoral positions are recruited after the end of their Ph.D. or after a first postdoctoral period: for the candidates who obtained their Ph.D. 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 that of the Ph.D. (and, if applicable, from the job held since the Ph.D.); particular attention is thus paid to French or international candidates who obtained their doctorate abroad.
Join with your application:
- Detailed CV with a description of the PhD and a complete list of publications with the two most significant ones highlighted
- A Motivation letter
- 2 letters of recommendations
- Passport copy
Contact informations:
- Elaine Pimentel, e.pimentel@ucl.ac.uk
- Alexis Saurin, alexis.saurin@inria.fr
Deadline for applying: June 1st 2025
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 : PICUBE
-
Recruiter :
Saurin Alexis / Alexis.Saurin@inria.fr
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.