on March 28, 2019 at 2:00 pm
Logipedia: Towards a wikipedia of formal demonstrations.
Formal demonstrations, that is to say computerized, have become a central tool in computing (safety, security, etc.) and mathematics. However, each system – Coq, HOL Light, Isabelle/HOL, PVS… – implements its language and theory, limiting the possibilities of interoperability between systems and the durability of these demonstrations. Logipedia is an encyclopedia, under construction, of formal demonstrations expressed in various theories. We will present this encyclopedia and discuss the scientific question behind this development: what is a theory?
Organic:
Gilles Dowek is currently Inria’s research director. Within the Deducteam project-team (Inria Saclay -Île-de-France), he conducted his research on the relationship between programming languages and mathematical language, on computerized systems for processing mathematical demonstrations and on the safety of software.
Previously, he was a researcher at the institute from 1993 to 2002, then a professor at the École Polytechnique from 2003 to 2010. He has also worked in the United States, at Carnegie Mellon University in Pittsburgh, in the laboratories of Computational Logic in Austin and at the NIA (National Institute for Aerospace, NASA) in Hampton.
Gilles Dowek is particularly committed to scientific mediation with the general public. He is the author of several popular books on mathematical sciences. In 2000, the Société mathématique de France awarded him the Grand Prix d’Alembert des Lycéens for his work in spreading mathematics to young people. He received the 2007 Grand Prize in Philosophy from the French Academy for «The metamorphoses of calculus, an astonishing history of mathematics» (éditions du Pommier).
More...Ircica, Villeneuve d'Ascq
français
English