Post-Doctoral Research Visit F/M Adapting Deep Inference for Induction and Co-Induction
Contract type : Fixed-term contract
Renewable contract : Yes
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 40 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
As part of an Exploratory Action (AEx) grant "IMPROOF"
- Members of the PARTOUT team (K. Chaudhuri - PI, B. Werner, L. Straßburger)
Goal: Develop foundations and build prototypes for direct manipulation proofs for induction and co-induction
Is regular travel foreseen for this post ? No.
English fluency required ? Yes. (Most collaborators are native English speakers.)
Assignment
Assignments :
The recruited person will work at the Inria Saclay research center (Alan Turing Building, co-located with LIX) as a member of the PARTOUT team.
For a better knowledge of the proposed research subject :
Please see the detailed program at the following URL:
http://www.lix.polytechnique.fr/~kaustuv/improof_postdoc_program.pdf
Collaboration :
In addition to the supervisor, the recruited person will collaborate with members of the EPC PARTOUT, primarily Prof. Benjamin Werner and Dr. Lutz Straßburger.
Responsibilities :
The person recruited will be in charge of developing techniques for adapting deep inference for induction and co-induction proofs as part of the "direct manipulation" cluster of interactive theorem proving techniques. This will involve significant work on the foundations and the theory of cyclic proofs. It is envisioned that there will also need to be some work done on incorporating theories and lemmas, and for the specification of new object proof systems.
The recruited person is also expected to participate in the design, implementation, and testing of software prototypes that are part of the "Profound" family of interactive tools.
Steering/Management :
The recruited person will be supervised by Dr. Kaustuv Chaudhuri.
Main activities
Skills
Languages : English
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
Remuneration
2788 € gross/month
General Information
- Theme/Domain :
Proofs and Verification
Software engineering (BAP E) - Town/city : Palaiseau
- Inria Center : Centre Inria de Saclay
- Starting date : 2024-08-01
- Duration of contract : 12 months
- Deadline to apply : 2024-06-30
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 (DGD-S)
-
Recruiter :
Chaudhuri Kaustuv / Kaustuv.Chaudhuri@inria.fr
The keys to success
Main requirements for this candidate:
- A PhD thesis in the area of structural proof theory
- Expertise with one or more deep inference formalisms
- Familiarity with a variety of mathematical and computational logics, in particular linear logic
An ideal candidate would also have:
- Experience with formal reasoning systems such as Coq, Lean, Isabelle/HOL
- Experience building prototype implementations of automated or interactive provers
- Experience with programming in OCaml or a similar functional language would be great, but not essential
- Experience with building user interfaces using JavaScript UI frameworks would be nice, but not essential
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.