Vous êtes ici

Post-doc in Formal Semantics and Compiler Verification


The IRISA/Inria Celtique group in Rennes has one open post-doctoral position. The position is funded by the national ANR project Discover (http://discover.irisa.fr/).

The Discover project leverages recent foundational work on formal verification and proof assistants to design, implement and verify compilation techniques for high-level programming languages. The project takes a resolute language-based approach, and investigates the formalisation of adequate program intermediate representations semantics, optimisations, and associated correctness proof techniques.

The long-term goal of the project is to devise formal proof techniques. This often requires prior explorations in the broader scope of language/IR semantic design, analysis, implementation, and empirical evaluation.


Possible research directions include, but are not limited to:

- Formal semantics (design and validation): explore how modern compilers IR can be used as a medium to express language-level semantics, and validate proposals by integrating them into existing tool frameworks.
- Formalisation and soundness proof of programming idioms, programming disciplines, and of modern compiler optimizations, with application to real-world case studies.

Profil / compétences: 

Applicants must have a PhD in Computer Science. We seek candidates with a strong background in Computer Science with an interest in at least one of the following topics: formal semantics, programming languages, compiler implementation. Applicants should have a strong theoretical background, but also some experience with software development.

The position is for one year minimum (with a possible extension) and the starting date is flexible -- to some extent. The working language is English, knowledge of French is not required.

The successful candidate will join the Celtique team at IRISA, INRIA Rennes: https://team.inria.fr/celtique/

Diplôme requis: 
PhD thesis in Computer Science
Lieu de travail: 
Rennes - France
Type de contrat: 
Funded by grant number ANR-14-CE28-0004
Durée du contrat (en mois): 
Corps / catégorie: 
Salaire Brut / Mens €: 
commensurate with qualifications and experience
Date prévisionnelle d'embauche: 
Flexible (to some extent)
Date limite de candidature: 
Jeudi, 31. mai 2018

Applicants should send their curriculum vitae, a cover letter and names/contact information of three references to delphine.demange@irisa.fr.
If possible, recommendation letters should be sent to Delphine Demange directly.
Please feel free to contact Delphine Demange for further information about the project, the position, or the research environment.