Charla: "Toward a next generation of proof assistants: going beyond the proofs as programs paradigm"
Nicolas Tabareau (Inria, Francia)

Abstract: In this talk, I will present several recent proposals to extend the power of proof assistants based on dependent type theory. I will review the current achievements and the missing pieces to integrate them properly in a real world proof assistant such as Coq, Lean or Agda. In particular, we will identity a fundamental lack of logical modularity as the main reason why few significant improvement have really been made in the last decades in mainstream proof assistants, and propose a solution to this issue.

Bio: Nicolas Tabareau is a Director of Research at Inria in France, head of the Gallinette research team who works on type theory and proof assistants, most notably the widely-used Coq proof assistant.

  • Tags

Auditorio Ramón Picarte
Facultad de Cs. Físicas y Matemáticas
Universidad de Chile

Beauchef 851, edificio norte, 3er piso

Fecha del evento
14 de Marzo de 2023
14:30 - 15:30

Éric Tanter