Write a Blog >>
Yves Bertot

Registered user since Wed 31 Aug 2016

Name:Yves Bertot

Research at Inria since 1992. co-author of a book on “Interactive Theorem Proving and Program Development, Coq’Art: the Calculus of Inductive Constructions”. Recipient of the 2013 ACM Software System award, along with developers of the Coq system.

Research interests:Interactive Theorem Proving, Higher-Order theorem proving


CPP 2020 Session Chair of Proof engineering and user interaction (part of CPP 2020)
CoqPL 2020 Session Chair of Invited Talk (part of CoqPL)
The use of Coq for Common Criteria Evaluations
Show activities from other conferences

POPL 2020-profile
View general profile