LEADER 02709oam  2200601   450 
001 996465848203316
005 20210716142137.0
010   $a3-540-48167-2
024 7 $a10.1007/3-540-48167-2
035   $a(CKB)1000000000211114
035   $a(SSID)ssj0000327466
035   $a(PQKBManifestationID)11245707
035   $a(PQKBTitleCode)TC0000327466
035   $a(PQKBWorkID)10301359
035   $a(PQKB)10139598
035   $a(DE-He213)978-3-540-48167-6
035   $a(MiAaPQ)EBC3072208
035   $a(MiAaPQ)EBC6486374
035   $a(PPN)155185039
035   $a(EXLCZ)991000000000211114
100   $a20210716d1999      uy             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 00$aTypes for proofs and programs $eInternational Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998 : selected papers /$fThorsten Altenkirch, Wolfgang Naraschewski, Bernhard Reus, editors
205   $a1st ed. 1999.
210  1$aBerlin ;$aHeidelberg :$cSpringer,$d[1999]
210  4$d©1999
215   $a1 online resource (VIII, 212 p.) 
225 1 $aLecture Notes in Computer Science ;$v1657
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-66537-4 
320   $aIncludes bibliographical references.
327   $aOn Relating Type Theories and Set Theories -- Communication Modelling and Context-Dependent Interpretation: An Integrated Approach -- Gröbner Bases in Type Theory -- A Modal Lambda Calculus with Iteration and Case Constructs -- Proof Normalization Modulo -- Proof of Imperative Programs in Type Theory -- An Interpretation of the Fan Theorem in Type Theory -- Conjunctive Types and SKInT -- Modular Structures as Dependent Types in Isabelle -- Metatheory of Verification Calculi in LEGO -- Bounded Polymorphism for Extensible Objects -- About Effective Quotients in Constructive Type Theory -- Algorithms for Equality and Unification in the Presence of Notational Definitions -- A Preview of the Basic Picture: A New Perspective on Formal Topology.
410  0$aLecture notes in computer science ;$v1657.
606   $aAutomatic theorem proving$vCongresses
606   $aType theory$vCongresses
615  0$aAutomatic theorem proving
615  0$aType theory
676   $a004.015113
701   $aAltenkirch$b Thorsten$f1962-$0930976
701   $aNaraschewski$b Wolfgang$f1970-$01252366
701   $aReus$b Bernhard$f1965-$0934969
712 12$aTYPES '98
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bUtOrBLW
906   $aBOOK
912   $a996465848203316
996   $aTypes for proofs and programs$92903403
997   $aUNISA