LEADER 00958nam a2200241 i 4500 001 991000391039707536 005 20020509165827.0 008 980219s1976 ||| ||| | ||| 020 $a385124057X 035 $ab11350362-39ule_inst 035 $aPARLA207210$9ExL 040 $aDip.to Filosofia$bita 245 10$aSprache und Erkenntnis :$bfestschrift fur Gerhard Frey zum 60. Geburtstag /$chrsg. von Bernulf Kanitscheider 260 $aInnsbruck :$bAmoe,$c1976 300 $a349 p. ;$c24 cm. 490 0 $aInnsbrucker beitrage zur kulturwissenschaft ;$v19 700 1$aKanitscheider, Bernulf$eauthor$4http://id.loc.gov/vocabulary/relators/aut 907 $a.b11350362$b01-03-17$c01-07-02 912 $a991000391039707536 945 $aLE005 55 A 224$g1$i2005000008566$lle005$o-$pE0.00$q-$rl$s- $t0$u0$v0$w0$x0$y.i11526488$z01-07-02 996 $aSprache und Erkenntnis$9825162 997 $aUNISALENTO 998 $ale005$b01-01-98$cm$da $e-$fger$gde $h0$i1 LEADER 05870nam 22008175 450 001 9910767505003321 005 20250415214231.0 010 $a9783540391852 010 $a3540391851 024 7 $a10.1007/3-540-39185-1 035 $a(CKB)1000000000212068 035 $a(SSID)ssj0000327460 035 $a(PQKBManifestationID)11276294 035 $a(PQKBTitleCode)TC0000327460 035 $a(PQKBWorkID)10301904 035 $a(PQKB)10493931 035 $a(DE-He213)978-3-540-39185-2 035 $a(MiAaPQ)EBC3071584 035 $a(PPN)155221191 035 $a(EXLCZ)991000000000212068 100 $a20121227d2003 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTypes for Proofs and Programs $eSecond International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers /$fedited by Herman Geuvers, Freek Wiedijk 205 $a1st ed. 2003. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2003. 215 $a1 online resource (CCCXLIV, 336 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v2646 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a9783540140313 311 08$a354014031X 320 $aIncludes bibliographical references and index. 327 $a(Co-)Iteration for Higher-Order Nested Datatypes -- Program Extraction in Simply-Typed Higher Order Logic -- General Recursion in Type Theory -- Using Theory Morphisms for Implementing Formal Methods Tools -- Subsets, Quotients and Partial Functions in Martin-Löf?s Type Theory -- Mathematical Quotients and Quotient Types in Coq -- A Constructive Formalization of the Fundamental Theorem of Calculus -- Two Behavioural Lambda Models -- A Unifying Approach to Recursive and Co-recursive Definitions -- Holes with Binding Power -- Typing with Conditions and Guarantees for Functional In-place Update -- A New Extraction for Coq -- Weak Transitivity in Coercive Subtyping -- The Not So Simple Proof-Irrelevant Model of CC -- Structured Proofs in Isar/HOL -- Java as a Functional Programming Language -- Monad Translating Inductive and Coinductive Types -- A Finite First-Order Presentation of Set Theory. 330 $aThese proceedings contain a refereed selection of papers presented at the Second Annual Workshop of the Types Working Group (Computer-Assisted Reasoning based on Type Theory, EUIST project 29001), which was held April 24?28, 2002 in Hotel Erica, Berg en Dal (close to Nijmegen), The Netherlands. The workshop was attended by about 90 researchers. On April 27, there was a special afternoon celebrating the 60th birthday of Per Martin-L¨of, one of the founding fathers of the Types community. The afternoon consisted of the following three invited talks: ?Constructive Validity Revisited? by Dana Scott, ?From the Rules of Logic to the Logic of Rules? by Jean-Yves Girard, and ?The Varieties of Type Theories? by Peter Aczel. The contents of these contributions were not laid down in these proceedings, but the videos of the talks and the slides used by the speakers are available at http://www. cs. kun. nl/fnds/MartinLoefDay/LoefTalks. htm The previous workshop of the Types Working Group under EUIST project 29001 was held in 2000 in Durham, UK. The workshops Types 2000 and Types 2002 followed a series of meetings organized in the period 1993 ? 1999 whithin previous Types projects (ESPRIT BRA 6435 and ESPRIT Working Group 21900). The proceedings of these earlier Types workshops were also published in the LNCS series, as volumes 806, 996, 1158, 1512, 1657, 1956 and 2277. ESPRIT BRA 6453 was a continuation of ESPRIT Action 3245, Logical Frameworks: - sign, Implementation and Experiments. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v2646 606 $aSoftware engineering 606 $aComputers 606 $aComputer logic 606 $aProgramming languages (Electronic computers) 606 $aLogic, Symbolic and mathematical 606 $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002 606 $aScience, Humanities and Social Sciences, multidisciplinary$3https://scigraph.springernature.com/ontologies/product-market-codes/A11007 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 615 0$aSoftware engineering. 615 0$aComputers. 615 0$aComputer logic. 615 0$aProgramming languages (Electronic computers) 615 0$aLogic, Symbolic and mathematical. 615 14$aSoftware Engineering/Programming and Operating Systems. 615 24$aScience, Humanities and Social Sciences, multidisciplinary. 615 24$aTheory of Computation. 615 24$aLogics and Meanings of Programs. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aMathematical Logic and Formal Languages. 676 $a005.1 702 $aGeuvers$b Herman$f1964-$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aWiedijk$b Freek$f1961-$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTYPES 2002 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910767505003321 996 $aTypes for Proofs and Programs$9771867 997 $aUNINA