Charla: CoqHoTT -- Coq for Homotopy Type Theory

Nicolas Tabareau, INRIA
11 Marzo, 2015 - 12:00
Auditorio DCC, Piso 4
PLEIAD / É. Tanter

The goal of the CoqHott project is to go further in the correspondence between proofs and programs which has allowed in the last 20 years the development of useful proof assistants, such as Coq (developed by Inria). Those assistants have shown their efficiency to prove correctness of important pieces of software but their democratization suffers from a major drawback, the mismatch between equality in mathematics and in type theory (which is the theory at the heart of Coq). Thus, significant Coq developments have only been done by virtuosos playing with advanced concepts of both computer science and mathematics. Recently, an extension of type theory with homotopical concepts has been proposed by Fields medal Vladimir Voevodsky, which allows for the first time to get the right notion of equality in theorem provers. The main goal of the CoqHoTT project is to provide a new generation of proof assistants based on this fascinating connection between homotopy theory and type theory.


In this talk, I will spend a long time presenting the basics of Type Theory and Homotopy Type Theory and try to present quickly the main goal of the CoqHoTT project.


About the speaker:


Nicolas Tabareau is an Inria researcher at École des Mines de Nantes since 2009.  He did a PhD at University Paris 7 on the semantics of programming languages.  He has been collaborating with members of PLEIAD for several years on  aspect-oriented programming and more recently on functional programming and  proof assistants. He has just obtained an ERC (European Research Council) grant to lead the CoqHoTT project for the period of 2015-2019