Phd Position F/m Verified Meta-programming for Proof Assistants

Le descriptif de l’offre ci-dessous est en Anglais_

**Type de contrat**: CDD

**Niveau de diplôme exigé**: Bac + 5 ou équivalent

**Fonction**: Doctorant

**Contexte et atouts du poste**:
The PhD will take place in the Cambium team at Inria Paris. Travel to conferences and workshops is usally possible.

**Mission confiée**:
**Assignments**:
The position consists of full-time research.

**Collaboration**:
Collaboration with other Inria teams and international collaborators will be possible.

**Principales activités**:
Main activities (5 maximum) : Analysis and comparison of existing meta-programming facilities in proof assistants. Establishment of MetaCoq as a meta-programming framework for Coq. Utilising dependent types for verifiable guarantees for meta-programs. Documentation of meta-programming in Coq. Writing of research articles on the results.

**Compétences**:
Technical skills and level required : Background in proof assistants based on type theory necessary. Knowledge of Coq beneficial. A good knowledge of functional programming (e.g. OCaml) is helpful.

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 (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
Calcul Scientifique (BAP E)
- **Ville**: Paris
- **Centre Inria**: Centre Inria de Paris
- **Date de prise de fonction souhaitée**: 2025-09-01
- **Durée de contrat**: 3 ans
- **Date limite pour postuler**: 2025-08-31

**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**: CAMBIUM
- **Directeur de thèse**:
**L'essentiel pour réussir**:
The prospective student should have a background in interactive theorem proving, ideally in a proof assistant based on type theory, e.g. Coq, Agda, or Lean. A good knowledge of functional programming is helpful.

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