Twenty-Five Years of Constructive Type Theory: Proceedings of a Congress held in Venice, October 1995

by Giovanni Sambin, Jan M. Smith, Jan Smith

Overview

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.

Product Details

ISBN-13:	9780198501275
Publisher:	OUP Oxford
Publication date:	10/28/1998
Series:	Oxford Logic Guides Series , #36
Pages:	296
Product dimensions:	6.30(w) x 9.30(h) x 0.80(d)

About the Author

University of Padua

Chalmers University of Technology

Table of Contents

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

Editorial Reviews

"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

From the Publisher