Twenty Five Years of Constructive Type Theory

Hardcover | August 1, 1998

byGiovanni Sambin, Jan M. Smith

not yet rated|write a review
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.

Pricing and Purchase Info

$135.95 online
$168.00 list price (save 19%)
Ships within 1-3 weeks
Ships free on orders over $25

From the Publisher

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 r...

Giovanni Sambin is at University of Padua. Jan Smith is at Chalmers University of Technology.

other books by Giovanni Sambin

The Basic Picture: Structures for Constructive Topology
The Basic Picture: Structures for Constructive Topology

Hardcover|Jul 30 2017

$125.98 online$126.00list price
Format: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

Reviews

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