Title: Logipedia: towards a Wikipedia of formal proofs

Speaker: Gilles Dowek (Inria and école normale supérieure de Paris-Saclay)

Time: 10:00 a.m. November 20th, 2019

Venue: Lecture room (334),  Building 5, SKLCS, Institute of Software, CAS

Abstract: Formal computerized proofs are now a central tool in computer science and in mathematics. But, each system – Coq, HOL Light, Isabelle/HOL, PVS... – implements its own language and its own theory, limiting the interoperability between systems and the sustainability of these proofs. Logipedia is an, in progress, encyclopedia of formal proofs, expressed in various theories. It is based on the idea to express these theories in a new logical framework allowing bound variables, explicit proof-terms, computation rules, and peaceful co-existence of constructive and non constructive proofs. 

Bio: Gilles Dowek is a senior researcher at Inria and professor at the école normale supérieure de Paris-Saclay. He is interested in the formalization of mathematics, in proof processing systems, in the physics of computation, in the safety of aerospace systems, and in the epistemology and ethics of computer science. He is a member of the Scientific board of the  French computer science society and of the CERNA ethics committee. He has contributed to the computer science curricula in French high schools. In the past, he has been Deputy Scientific Director of Inria in charge of the domain Algorithmic, Programming, Software and Architectures. His book Les Métamorphoses du calcul (the metamorphoses of calculation) was awarded le Grand Prix de philosophie 2007 de l’Académie fran？aise. http://www.lsv.fr/~dowek/