Yves Bertot -

Registered user since Wed 31 Aug 2016

Name:Yves Bertot

Bio:

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.

Country:France

Affiliation:INRIA

Personal website:http://www-sop.inria.fr/members/Yves.Bertot/index.html

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

Contributions

CoqPL 2023	Speaker of Session with the Coq Development Team within the CoqPL 2023-track
CoqPL 2022	Speaker of Session with the Coq Development Team within the CoqPL-track
CPP 2022	Committee Member in Program Committee within the CPP 2022-track
CPP 2020	Session Chair of Proof engineering and user interaction (part of CPP 2020)
CoqPL 2020	Session Chair of Invited Talk (part of CoqPL) Author of The use of Coq for Common Criteria Evaluations within the CoqPL-track
CoqPL 2018	Programme Co-Chair in Program Committee within the -track Programme Co-Chair in Organizing Committee within the -track Author of Session with the Coq Development Team within the -track Session Chair of Keynote (part of )
CPP 2017	Co-chair in Program Committee within the CPP-track
CPP 2016	Author of Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials within the CPP-track