Twenty Five Years of Constructive Type Theory by Giovanni Sambin

Twenty Five Years of Constructive Type Theory

byGiovanni Sambin, Jan M. Smith

Hardcover | August 1, 1998

not yet rated|write a review

Pricing and Purchase Info

$135.01 online 
Earn 675 plum® points

In stock online

Ships free on orders over $25

Not available in stores


Per Martin-Lof's work on the development of constructive type theory has been of huge significance in the fields of logic and the foundations of mathematics. It is also of broader philosophical significance, and has 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-Lof 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 aninvaluable record of areas of current activity, but also contains 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-Lof's earliest papers.

About The Author

Giovanni Sambin is at University of Padua. Jan Smith is at Chalmers University of Technology.
The Basic Picture: Structures for Constructive Topology
The Basic Picture: Structures for Constructive Topology

by Giovanni Sambin


Pre-order online

Not yet available in stores

Details & Specs

Title:Twenty Five Years of Constructive Type TheoryFormat:HardcoverPublished:August 1, 1998Publisher:Oxford University PressLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:0198501277

ISBN - 13:9780198501275

Look for similar items by category:

Customer Reviews of Twenty Five Years of Constructive Type Theory


Extra Content

Table of Contents

1. Yet another constructivization of classical logic2. Extension of Martin-Lof's type theory with record types3. Type-theoretical checking and philosophy of mathematics4. The Hahn-Banach theorem in type theory5. A realizability interpretation of Martin-Lof's type theory6. The groupoid interpretation of type theory7. An intuitionistic theory of types8. Analytic program derivation in type theory9. About storage operators10. On universes in type theory11. How to believe a machine-checked proof12. Building up a toolbox for Martin-Lof's type theory: subset theory13. An introduction to well-ordering proofs in Martin-Lof's type theory14. Variable-free formalization of the Curry-Howard theory15. The forget-restore principle: a paradigmatic example

Editorial Reviews

`The book presents a good survey of the current state of the subject.'EMS Newsletter