By continuing to browse the site, you are agreeing to our use of cookies. (More details)

POST DOCTORAL RESEARCHER M/F – Post-doctoral researcher in logic and verification - LYON

This offer is available in the following languages:
Français - Anglais

Ensure that your candidate profile is correct before applying. Your profile information will be added to the details for each application. In order to increase your visibility on our Careers Portal and allow employers to see your candidate profile, you can upload your CV to our CV library in one click!

Faites connaître cette offre !

General information

Reference : UMR5668-MARNAR-007
Workplace : LYON 07
Date of publication : Thursday, July 16, 2020
Type of Contract : FTC Scientist
Contract Period : 12 months
Expected date of employment : 1 October 2020
Proportion of work : Full time
Remuneration : Between 2675 à 3805€ gross monthly salary according to experience
Desired level of education : PhD
Experience required : 1 to 4 years


The selected candidate will be hired for a 12 months post-doc, in order to conduct original research within the CoVeCe project (Coinduction for Verification and Certification – ERC starting grant).
The research will be done within the LIP laboratory (ENS - Lyon, France) in the Plume team, under the supervision of Damien Pous (CNRS senior researcher).


The objective is to study proof systems and algorithms for certain extensions of Kleene algebras, and to implement the resulting theorems and tools inside the Coq proof assistant.
Depending on the candidate, the research will be oriented towards the logical aspects of the problem, towards its algorithmic aspects, or toward formalisation in Coq.


The candidates must have obtained a PhD in theoretical computer science. Ideally, the candidate will already master some of the following topics: automata, Kleene algebra, proof systems, bounded treewidth graphs, coinduction, proof assistants.

Work Context

The research will be made at the LIP laboratory (ENS - Lyon, France) within the Plume team, under the supervision of Damien Pous (CNRS senior researcher) for his ERC starting grant 'CoVeCe'.
The Plume team works in the mathematical foundations of software correctness: type systems, logic, linear logic, process calculi, model verification, proof assistants, implicit complexity.
The CoVeCe project focuses on applications of coinduction and automata algorithms to ease certain verification tasks, and their certification via formalisation in proof assistants like Coq.

Constraints and risks

The LIP laboratory is not an experimental laboratory and does not incur specific risks or constraints.

Additional Information

Find out more about ERC CoVeCe

We talk about it on Twitter!