LEADER 05386nam 22007815 450 001 9910143606303321 005 20251116234142.0 010 $a3-540-44557-9 024 7 $a10.1007/3-540-44557-9 035 $a(CKB)1000000000211392 035 $a(SSID)ssj0000327458 035 $a(PQKBManifestationID)11232129 035 $a(PQKBTitleCode)TC0000327458 035 $a(PQKBWorkID)10301734 035 $a(PQKB)10945426 035 $a(DE-He213)978-3-540-44557-9 035 $a(MiAaPQ)EBC3073178 035 $a(PPN)155219251 035 $a(BIP)7043989 035 $a(EXLCZ)991000000000211392 100 $a20121227d2000 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTypes for Proofs and Programs $eInternational Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers /$fedited by Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan Smith 205 $a1st ed. 2000. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2000. 215 $a1 online resource (VIII, 197 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1956 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-540-41517-3 320 $aIncludes bibliographical references at the end of each chapters and index. 327 $aSpecification and Verification of a Formal System for Structurally Recursive Functions -- A Predicative Strong Normalisation Proof for a ?Calculus with Interleaving Inductive Types -- Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and ?-Rule -- Computer-Assisted Mathematics at Work -- Specification of a Smart Card Operating System -- Implementation Techniques for Inductive Types in Plastic -- A Co-inductive Approach to Real Numbers -- Information Retrieval in a Coq Proof Library Using Type Isomorphisms -- Memory Management: An Abstract Formulation of Incremental Tracing -- The Three Gap Theorem (Steinhaus Conjecture) -- Formalising Formulas-as-Types-as-Objects. 330 $aThis book contains a selection of papers presented at the third annual workshop of the Esprit Working Group 21900 Types, which was held 12 - 16 June 1999 at L¨okeberg in the rural area north of G¨oteborg and close to Marstrand. It was attended by 77 researchers. The two previous workshops of the working group were held in Aussois, France, in December 1996 and in Irsee, Germany, in March 1998. The proc- dings of those workshops appear as LNCS Vol. 1512 (edited by Christine Paulin- Mohring and Eduardo Gimenez) and LNCS Vol. 1657 (edited by Thorsten - tenkirch, Wolfgang Naraschewski, and Bernhard Reus). These workshops are, in turn, a continuation of the meetings organized in 1993, 1994, and 1995 under the auspices of the Esprit Basic Research Action 6453 Types for Proofs and Programs. Those proceedings were also published in the LNCS series, edited by Henk Barendregt and Tobias Nipkow (Vol. 806, 1993), by Peter Dybjer, Bengt Nordstr¨om, and Jan Smith (Vol. 996, 1994) and by Stefano Berardi and Mario Coppo (Vol. 1158, 1995). The Esprit BRA 6453 was a continuation of the former Esprit Action 3245 Logical Frameworks: - sign, Implementation and Experiments. The articles from the annual workshops organized under that Action were edited by Gerard Huet and Gordon Plotkin in the books Logical Frameworks and Logical Environments, both published by Cambridge University Press. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v1956 606 $aProgramming languages (Electronic computers) 606 $aComputer logic 606 $aLogic, Symbolic and mathematical 606 $aArtificial intelligence 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 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 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aMathematical Logic and Foundations$3https://scigraph.springernature.com/ontologies/product-market-codes/M24005 615 0$aProgramming languages (Electronic computers) 615 0$aComputer logic. 615 0$aLogic, Symbolic and mathematical. 615 0$aArtificial intelligence. 615 14$aProgramming Languages, Compilers, Interpreters. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 615 24$aMathematical Logic and Foundations. 676 $a005.13/1 702 $aCoquand$b Thierry$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aDybjer$b Peter$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aNordström$b Bengt$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSmith$b Jan$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTYPES '99 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910143606303321 996 $aTypes for Proofs and Programs$9771867 997 $aUNINA