LEADER 04271nam  22006975  450 
001 996466249703316
005 20200630171134.0
010   $a3-540-48440-X
024 7 $a10.1007/3-540-58085-9
035   $a(CKB)1000000000234119
035   $a(SSID)ssj0000327462
035   $a(PQKBManifestationID)11273414
035   $a(PQKBTitleCode)TC0000327462
035   $a(PQKBWorkID)10301523
035   $a(PQKB)11539463
035   $a(DE-He213)978-3-540-48440-0
035   $a(PPN)155174630
035   $a(EXLCZ)991000000000234119
100   $a20121227d1994      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 '93, Nijmegen, The Netherlands, May 24 - 28, 1993. Selected Papers /$fedited by Henk Barendregt, Tobias Nipkow
205   $a1st ed. 1994.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1994.
215   $a1 online resource (IX, 395 p.) 
225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v806
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-58085-9 
327   $aProving strong normalization of CC by modifying realizability semantics -- Checking algorithms for Pure Type Systems -- Infinite objects in type theory -- Conservativity between logics and typed ? calculi -- Logic of refinement types -- Proof-checking a data link protocol -- Elimination of extensionality in Martin-Löf type theory -- Programming with streams in Coq a case study: The Sieve of Eratosthenes -- The Alf proof editor and its proof engine -- Encoding Z-style Schemas in type theory -- The expressive power of Structural Operational Semantics with explicit assumptions -- Developing certified programs in the system Coq the program tactic -- Closure under alpha-conversion -- Machine Deduction -- Type theory and the informal language of mathematics -- Semantics for abstract clauses.
330   $aThis volume contains thoroughly refereed and revised full papers selected from the presentations at the first workshop held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs in Nijmegen, The Netherlands, in May 1993. As the whole ESPRIT BRA 6453, this volume is devoted to the theoretical foundations, design and applications of systems for theory development. Such systems help in designing mathematical axiomatisation, performing computer-aided logical reasoning, and managing databases of mathematical facts; they are also known as proof assistants or proof checkers.
410  0$aLecture Notes in Computer Science,$x0302-9743 ;$v806
606   $aComputers
606   $aSoftware engineering
606   $aMathematical logic
606   $aComputer logic
606   $aArtificial intelligence
606   $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005
606   $aSoftware Engineering/Programming and Operating Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I14002
606   $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048
606   $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X
606   $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000
615  0$aComputers.
615  0$aSoftware engineering.
615  0$aMathematical logic.
615  0$aComputer logic.
615  0$aArtificial intelligence.
615 14$aTheory of Computation.
615 24$aSoftware Engineering/Programming and Operating Systems.
615 24$aMathematical Logic and Formal Languages.
615 24$aLogics and Meanings of Programs.
615 24$aArtificial Intelligence.
676   $a005.1/01/5113
702   $aBarendregt$b Henk$4edt$4http://id.loc.gov/vocabulary/relators/edt
702   $aNipkow$b Tobias$4edt$4http://id.loc.gov/vocabulary/relators/edt
906   $aBOOK
912   $a996466249703316
996   $aTypes for Proofs and Programs$9771867
997   $aUNISA