LEADER 03126nam 2200661Ia 450 001 9910780897403321 005 20230421050100.0 010 $a0-19-191654-4 010 $a1-280-81972-3 010 $a9786610819720 010 $a0-19-158903-9 035 $a(CKB)2450000000000611 035 $a(EBL)684605 035 $a(OCoLC)714569778 035 $a(SSID)ssj0000312128 035 $a(PQKBManifestationID)11207367 035 $a(PQKBTitleCode)TC0000312128 035 $a(PQKBWorkID)10329491 035 $a(PQKB)10483992 035 $a(MiAaPQ)EBC684605 035 $a(StDuBDS)EDZ0002338645 035 $a(Au-PeEL)EBL684605 035 $a(CaPaEBR)ebr10464228 035 $a(CaONFJC)MIL81972 035 $a(EXLCZ)992450000000000611 100 $a19980622d1998 uy 0 101 0 $aeng 135 $aur||||||||||| 181 $ctxt 182 $cc 183 $acr 200 00$aTwenty-five years of constructive type theory$b[electronic resource] $eproceedings of a congress held in Venice, October 1995 /$fedited by Giovanni Sambin and Jan M. Smith 210 $aOxford $cClarendon Press ;$aNew York $cOxford University Press$d1998 215 $a1 online resource (292 p.) 225 1 $aOxford logic guides ;$v36 225 1 $aOxford science publications 300 $aPreviously issued in print: Oxford: Clarendon Press, 1998. 311 $a0-19-850127-7 320 $aIncludes bibliographical references. 327 $aCover; 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 proof 327 $a12. 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 example 330 8 $aMartin-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. 410 0$aOxford logic guides ;$v36. 410 0$aOxford science publications. 606 $aType theory$vCongresses 606 $aLogic, Symbolic and mathematical$vCongresses 615 0$aType theory 615 0$aLogic, Symbolic and mathematical 676 $a511.3 701 $aSambin$b Giovanni$051923 701 $aSmith$b Jan M$0628862 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910780897403321 996 $aTwenty-five years of constructive type theory$93787730 997 $aUNINA