Twenty-Five Years of Constructive Type Theory

Proceedings of a Congress held in Venice, October 1995

Giovanni Sambin and Jan M. Smith

A Clarendon Press Publication

Twenty-Five Years of Constructive Type Theory

Proceedings of a Congress held in Venice, October 1995

Giovanni Sambin and Jan M. Smith

A Clarendon Press Publication

Description

Per Martin-Löf's work on the development of constructive type theory has had a tremendous impact on the fields of logic and the foundations of mathematics. It also has broader philosophical significance and important applications in areas such as computing science and linguistics. This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Löf over the last twenty-five years. As well as celebrating the anniversary of the birth of the subject it covers many of the diverse fields which are now influenced by type theory. It is an invaluable record of current activity and includes contributions from N. G. de Bruijn and William Tait, both important figures in the early development of the subject. Also published for the first time is one of Per Martin-Löf's earliest papers.

Twenty-Five Years of Constructive Type Theory

Proceedings of a Congress held in Venice, October 1995

Giovanni Sambin and Jan M. Smith

A Clarendon Press Publication

Oxford Logic Guides

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

Twenty-Five Years of Constructive Type Theory

Proceedings of a Congress held in Venice, October 1995

Giovanni Sambin and Jan M. Smith

A Clarendon Press Publication

Oxford Logic Guides

Author Information

Contributors:

Contributors - Page 1

Twenty-Five Years of Constructive Type Theory

Proceedings of a Congress held in Venice, October 1995

Giovanni Sambin and Jan M. Smith

A Clarendon Press Publication

Oxford Logic Guides

Reviews and Awards

"This is a fine collection of essays about and around Per Martin Ld"of's intuitionistic theory. This book is certainly a testimony to the vitality and fruitfulness of Martin-Ld"of's ideas in the foundations of mathematics and theoretical computer science." -- Yvon Gauthier, Modern Logic, Vol 8, No 1/2 (Jan 98 - Apr 2000) 2000

"This work has made an important contribution to the fields of logic and the foundations of mathematics and is also of broader philosophical significance. Its depth and relevance can be seen by its increasing application to a variety of fields from computing science to linguistics."--athematical Reviews