You are here

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 (

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.

Requirement and Profile: 

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:

Required Diploma: 
PhD thesis in Computer Science
Lieu de travail: 
Rennes - France
Type of contrat: 
Funded by grant number ANR-14-CE28-0004
Durée du contrat (en mois): 
Salary (before tax) / Month €: 
commensurate with qualifications and experience
Date prévisionnelle d'embauche: 
Flexible (to some extent)
Date limite de candidature: 
Thursday, 31. May 2018
How to apply: 

Applicants should send their curriculum vitae, a cover letter and names/contact information of three references to
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.