Publication of the inaugural lecture by Professor Thierry Coquand

Thierry Coquand

Type theory, from Russell to proof assistants

This book traces the recent history of type theory, from the verification of proofs on computers to the synergy between dependent type theory and homotopy theory.

Introduced by Bertrand Russell to avoid the paradoxes that arise in mathematics when the notion of a collection of objects is used too naively, type theory has been refined by the notion of dependent type. In addition to its important role in formalizing mathematical proofs, this notion is also of intrinsic conceptual interest in logic and computer science. This book traces the recent history of these discoveries, from the verification of proofs on computers to the synergy now being established between dependent type theory and homotopy theory.

Coquand T., La Théorie des types, de Russell aux assistants à la démonstration, Paris, Collège de France, coll. " Leçons inaugurales ", ^no 336, 2026, 64   p.

ISBN : 978-2-7226-0873-3
Price : 12  €
Publication : 19  March 2026

Thierry Coquand has been Professor of Computer Science at the University of Gothenburg (Sweden) since 1996. Recipient of the Kurt Gödel Centenary Research Award in 2008 for his research in logic and of the ACM SIGPLAN Programming Languages Software Award in 2013 for his work on proof assistants, he has been appointed visiting professor at the Collège de France on the Computer Sciences and Digital Technologies Annual Chair, created in partnership with Inria, for the academic year 2024-2025.