Summary
The last seminar concluded the series with a personal perspective on the history and current state of type theory. The speaker returned to his invention with Huet of the calculus of constructions, the formalism at the basis of the Coq proof assistant. The calculus of constructions emerged as a synthesis between de Bruijn's work on the Automath system for the mechanization of mathematics, Girard's work on the Fω system, and Martin-Löf's work on his type theory. Today, these formalisms are leading to a new and promising approach to the mathematical notion of identification between two collections, generalizing the notions of isomorphisms between algebraic structures and transport of properties.
