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.