Post-Doctoral Research Visit F/M Adapting Deep Inference for Induction and Co-Induction

Télécharger l'offre au format PDF
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD

Contrat renouvelable : Oui

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

Contexte et atouts du poste

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

Mission confiée

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.

Principales activités

 

 

Compétences

Languages : English

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

Rémunération

2788 € gross/month