UID:
edocfu_9959235831502883
Format:
1 online resource (292 p.)
Edition:
1st ed.
ISBN:
0-19-191654-4
,
1-280-81972-3
,
9786610819720
,
0-19-158903-9
Series Statement:
Oxford logic guides ; 36
Content:
Martin-LoÌf type theory is an important and practical formalisation of the foundations of mathematics. This volume celebrates the 25th anniversary of the birth of the subject, and is a record of areas of activity and of its early development.
Note:
Previously issued in print: Oxford: Clarendon Press, 1998.
,
Cover; Contents; 1. Yet another constructivization of classical logic; 2. Extension of Martin-Löf's type theory with record types and subtyping; 3. Type-theoretical checking and philosophy of mathematics; 4. The Hahn-Banach theorem in type theory; 5. A realizability interpretation of Martin-Löf's type theory; 6. The groupoid interpretation of type theory; 7. Analytic program derivation in type theory; 8. An intuitionistic theory of types; 9. On storage operators; 10. On universes in type theory; 11. How to believe a machine-checked proof
,
12. Building up a toolbox for Martin-Löf's type theory: subset theory13. An introduction to well-ordering proofs in Martin-Löf's type theory; 14. Variable-free formalization of the Curry-Howard theory; 15. The forget-restore principle: a paradigmatic example
,
English
Additional Edition:
ISBN 0-19-850127-7
Language:
English
