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

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

by Giovanni Sambin, Jan M. Smith
     
 

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

See more details below

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)

Meet 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

Read More

Customer Reviews

Average Review:

Write a Review

and post it to your social network

     

Most Helpful Customer Reviews

See all customer reviews >