03126nam 2200661Ia 450 991078089740332120230421050100.00-19-191654-41-280-81972-397866108197200-19-158903-9(CKB)2450000000000611(EBL)684605(OCoLC)714569778(SSID)ssj0000312128(PQKBManifestationID)11207367(PQKBTitleCode)TC0000312128(PQKBWorkID)10329491(PQKB)10483992(MiAaPQ)EBC684605(StDuBDS)EDZ0002338645(Au-PeEL)EBL684605(CaPaEBR)ebr10464228(CaONFJC)MIL81972(EXLCZ)99245000000000061119980622d1998 uy 0engur|||||||||||txtccrTwenty-five years of constructive type theory[electronic resource] proceedings of a congress held in Venice, October 1995 /edited by Giovanni Sambin and Jan M. SmithOxford Clarendon Press ;New York Oxford University Press19981 online resource (292 p.)Oxford logic guides ;36Oxford science publicationsPreviously issued in print: Oxford: Clarendon Press, 1998.0-19-850127-7 Includes bibliographical references.Cover; Contents; 1. Yet another constructivization of classical logic; 2. Extension of Martin-Lö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-Lö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 proof12. Building up a toolbox for Martin-Löf's type theory: subset theory13. An introduction to well-ordering proofs in Martin-Löf's type theory; 14. Variable-free formalization of the Curry-Howard theory; 15. The forget-restore principle: a paradigmatic exampleMartin-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.Oxford logic guides ;36.Oxford science publications.Type theoryCongressesLogic, Symbolic and mathematicalCongressesType theoryLogic, Symbolic and mathematical511.3Sambin Giovanni51923Smith Jan M628862MiAaPQMiAaPQMiAaPQBOOK9910780897403321Twenty-five years of constructive type theory3787730UNINA