Twenty-five years of constructive type theory [[electronic resource] ] : proceedings of a congress held in Venice, October 1995 / / edited by Giovanni Sambin and Jan M. Smith

• Pubblicazione: Oxford, : Clarendon Press; New York, : Oxford University Press, 1998
• Descrizione fisica: 1 online resource (292 p.)
• Disciplina: 511.3
• Soggetto topico: Type theory; Logic, Symbolic and mathematical
• Altri autori: SambinGiovanni SmithJan M
• Note generali: Previously issued in print: Oxford: Clarendon Press, 1998.
• Nota di bibliografia: Includes bibliographical references.
• Nota di contenuto: 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
• Sommario/riassunto: Martin-Lö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.
• Titolo autorizzato: Twenty-five years of constructive type theory
• ISBN: 0-19-191654-4; 1-280-81972-3; 9786610819720; 0-19-158903-9
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910780897403321
• Lo trovi qui: Univ. Federico II
• Serie: Oxford logic guides ; ; 36.; Oxford science publications.