Twenty Five Years of Constructive Type Theory by Giovanni SambinTwenty 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

Pricing and Purchase Info


Earn 840 plum® points

Prices and offers may vary in store


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.
Giovanni Sambin is at University of Padua. Jan Smith is at Chalmers University of Technology.
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:


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