Positions will remain continuously open until the end of March 2019 (or until fulfilled).

We are looking for interns to work with us on various aspects of the project. The typical duration of this temporary positions is between 2 and 5 months.

The long-term goal of the project is formal proof techniques. This often requires prior explorations in the broader scope of language/intermediate representations 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.


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 starting dates are 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:

Applicants should send their Curriculum Vitae, Cover Letter and names/contact information of three references to Delphine Demange. If possible, recommandation letters should be sent directly to Delphine Demange. Please feel free to contact Delphine Demange for further information about the project, the position, or the research environment.

Last Updated 2019-09-27 Fri 19:02