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, concurrent and managed 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 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 a validation of proposals by integrating into existing tool frameworks.

- Formalisation and soundness proof of programming idioms and disciplines, and 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. A background in concurrent programming languages would be ideal. 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: 
Le plus tôt possible
Date limite de candidature: 
Mercredi, 31. janvier 2018

Applicants should send their Curriculum Vitae, Cover Letter and names/contact information of three references to delphine.demange@irisa.fr
If possible, recommandation 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.