Faites connaître cette offre !
Reference : UMR5668-MARNAR-005
Workplace : LYON 07
Date of publication : Friday, November 29, 2019
Type of Contract : FTC Scientist
Contract Period : 12 months
Expected date of employment : 2 January 2020
Proportion of work : Full time
Remuneration : 3766 € gross monthly salary
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.
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.
We talk about it on Twitter!