You are here

Post-doc in Formal Semantics and Compiler Verification

Place: 
Context: 

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.

Mission: 

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.

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

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): 
12
Quotité: 
100%
Category: 
Post-doctoral
Salary (before tax) / Month €: 
commensurate with qualifications and experience
Date prévisionnelle d'embauche: 
Le plus tôt possible
Date limite de candidature: 
Sunday, 31. December 2017
How to apply: 

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.