1. Yet another constructivization of classical logic, Stefano Baratella and Stefano Berardi 2. Extension of Martin-Löf's type theory with record types and subtyping, Gustavo Betarte and Alvaro Tasistro 3. Type-theoretical checking and philosophy of mathematics, Nicolaas Govert de Bruijn 4. The Hahn-Banach theorem in type theory, Jan Cederquist, Thierry Coquand, and Sara Negri 5. A realizability interpretation of Martin-Löf's type theory, Catarina Coquand 6. The groupoid interpretation of type theory, Martin Hofmann and Thomas Streicher 7. An intuitionistic theory of types, Per Martin-Löf 8.

Analytic program derivation in type theory, Petri Mäenpää 9. About storage operators, Karim Nour 10. On universes in type theory, Erik Palmgren 11. How to believe a machine-checked proof, Robert Pollack 12. Building up a toolbox for Martin-Löf's type theory: subset theory, Giovanni Sambin and Silvio Valentini 13. An introduction to well-ordering proofs in Martin-Löf's type theory, Anton Setzer 14. Variable-free formalization of the Curry-Howard theory, William W. Tait 15.

The forget-restore principle: a paradigmatic example, Silvio Valentini.