LEADER 04617nam 22007095 450 001 996465945603316 005 20200701031358.0 010 $a3-540-49562-2 024 7 $a10.1007/BFb0097782 035 $a(CKB)1000000000548905 035 $a(SSID)ssj0000327465 035 $a(PQKBManifestationID)11266285 035 $a(PQKBTitleCode)TC0000327465 035 $a(PQKBWorkID)10301735 035 $a(PQKB)10757693 035 $a(DE-He213)978-3-540-49562-8 035 $a(PPN)155209833 035 $a(EXLCZ)991000000000548905 100 $a20121227d1998 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTypes for Proofs and Programs$b[electronic resource] $eInternational Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers /$fedited by Eduardo Gimenez, Christine Paulin-Mohring 205 $a1st ed. 1998. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1998. 215 $a1 online resource (VIII, 380 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1512 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-65137-3 327 $aCoercion synthesis in computer implementations of type-theoretic frameworks -- Verification of the interface of a small proof system in coq -- An implementation of the Heine-Borel covering theorem in type theory -- Detecting and removing dead-code using rank 2 intersection -- A type-free formalization of mathematics where proofs are objects -- Higman's lemma in type theory -- A proof of weak termination of typed ??-calculi -- Proof style -- Some algorithmic and proof-theoretical aspects of coercive subtyping -- Semantical BNF -- The internal type theory of a Heyting pretopos -- Inverting inductively defined relations in LEGO -- A generic normalisation proof for pure type systems -- Proving a real time algorithm for ATM in Coq -- Dependent types with explicit substitutions: A meta-theoretical development -- Type inference verified: Algorithm W in Isabelle/HOL -- Continuous lattices in formal topology -- Abstract insertion sort in an extension of type theory with record types and subtyping. 330 $aThis book constitutes the thoroughly revised post-workshop proceedings of the first annual workshop held under the auspices of the ESPRIT Working Group 21900 TYPES in Aussois, France in December 1996. The 18 revised full papers presented in the book were carefully reviewed and selected from the 30 papers accepted for presentation at the workshop. All current aspects of type theory and type systems and their applications to program verification and theorem proving are addressed; the proof systems and theorem provers dealt with include Coq, LEGO, and Isabelle/HOL. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v1512 606 $aSoftware engineering 606 $aComputer logic 606 $aMathematical logic 606 $aProgramming languages (Electronic computers) 606 $aArtificial intelligence 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 615 0$aSoftware engineering. 615 0$aComputer logic. 615 0$aMathematical logic. 615 0$aProgramming languages (Electronic computers). 615 0$aArtificial intelligence. 615 14$aSoftware Engineering/Programming and Operating Systems. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aArtificial Intelligence. 676 $a004/.01/5113 702 $aGimenez$b Eduardo$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aPaulin-Mohring$b Christine$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Workshop TYPES '96 906 $aBOOK 912 $a996465945603316 996 $aTypes for Proofs and Programs$9771867 997 $aUNISA