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

by Giovanni Sambin, Jan M. 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:	Oxford University Press
Publication date:	12/10/1998
Series:	Oxford Logic Guides , #36
Pages:	292
Product dimensions:	9.21(w) x 6.14(h) x 0.69(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 Berardi2. Extension of Martin-Löf's type theory with record types and subtyping, Gustavo Betarte and Alvaro Tasistro3. Type-theoretical checking and philosophy of mathematics, Nicolaas Govert de Bruijn4. The Hahn-Banach theorem in type theory, Jan Cederquist, Thierry Coquand, and Sara Negri5. A realizability interpretation of Martin-Löf's type theory, Catarina Coquand6. The groupoid interpretation of type theory, Martin Hofmann and Thomas Streicher7. An intuitionistic theory of types, Per Martin-Löf8. Analytic program derivation in type theory, Petri Mäenpää9. About storage operators, Karim Nour10. On universes in type theory, Erik Palmgren11. How to believe a machine-checked proof, Robert Pollack12. Building up a toolbox for Martin-Löf's type theory: subset theory, Giovanni Sambin and Silvio Valentini13. An introduction to well-ordering proofs in Martin-Löf's type theory, Anton Setzer14. Variable-free formalization of the Curry-Howard theory, William W. Tait15. The forget-restore principle: a paradigmatic example, Silvio Valentini

Editorial Reviews

"This is a fine collection of essays about and around Per Martin Ldof's intuitionistic theory. This book is certainly a testimony to the vitality and fruitfulness of Martin-Ldof'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