Postdoctoral position in formal semantics and compiler verification

The IRISA/Inria Celtique group in Rennes (France) 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
 validate proposals by an integration into existing tool frameworks.
- Formalisation and soundness proof of programming idioms and
 disciplines, and application to real-world case studies.

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/

Applicants should send their curriculum vitae, cover letter and
names/contact information of three references to Delphine Demange
([email protected]). 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.