CoVeCeCoinduction for Verification and Certification 
The aim of this ERC project is to exploit the unsung power of coinduction to improve upon the state of the art in verification and certification. The project is rather openended and goes from theory (category theory, coinduction) to practice (concrete implementations and linking with existing software). We plan to work on the following topics:
Automata algorithms  Calculus of relations  Proof assistants (Coq) 

Together with Filippo Bonchi, we have recently found a new
algorithm for language equivalence of finite automata on
strings [1]. This algorithm
exploits bisimulations up to congruence, and improves
existing algorithms by an order of magnitude.

Here we study the theory of binary relations and their
standard operations (union, composition, transitive closure,
converse...).

Proof assistants should help the user to write its proof.
To this end, one needs to provide powerful automation tools.
By certifying our results about automata and the calculus of relations, we aim at

¡ Open positions !We currently (as of 2019/09) have two open postdoc positions. We look for candidates with a strong background in one of the three above fields: automata theory, proof theory, proof assistants. Mastering those three fields simultaneously is not required! Please do apply by sending me an email with your motivations (which part(s) of the project you would like to be involved in, why...), a brief CV, and the names of two persons who could recommend you. Also please feel free to engage a scientific discussion, ask me directly for more details on the project, the salaries, the surrounding team (Plume), the lab (LIP), or the city of Lyon. 
Team
Past members

Close collaborators

References
