LEADER 04424nam  22007455  450 
001 996465771703316
005 20200702125330.0
010   $a3-540-47770-5
024 7 $a10.1007/3-540-60579-7
035   $a(CKB)1000000000234368
035   $a(SSID)ssj0000327463
035   $a(PQKBManifestationID)11247114
035   $a(PQKBTitleCode)TC0000327463
035   $a(PQKBWorkID)10297592
035   $a(PQKB)10616989
035   $a(DE-He213)978-3-540-47770-9
035   $a(PPN)155197851
035   $a(EXLCZ)991000000000234368
100   $a20121227d1995      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 '94, Bastad, Sweden, June 6-10, 1994. Selected Papers /$fedited by Peter Dybjer, Bengt Nordström, Jan Smith
205   $a1st ed. 1995.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1995.
215   $a1 online resource (X, 210 p.) 
225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v996
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-60579-7 
327   $aCommunicating contexts: A pragmatic approach to information exchange -- A short and flexible proof of strong normalization for the calculus of constructions -- Codifying guarded definitions with recursive schemes -- The metatheory of UTT -- A user's friendly syntax to define recursive functions as typed ?-terms -- I/O automata in Isabelle/HOL -- A concrete final coalgebra theorem for ZF set theory -- On extensibility of proof checkers -- Syntactic categories in the language of mathematics -- Formalization of a ?-calculus with explicit substitutions in Coq.
330   $aThis book presents a strictly refereed collection of revised full papers selected from the papers accepted for the TYPES '94 Workshop, held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs in Bastad, Sweden, in June 1994. The 10 papers included address various aspects of developing computer-assisted proofs and programs using a logical framework. Type theory and three logical frameworks based on it are dealt with: ALF, Coq, and LEGO; other topics covered are metatheory, the Isabelle system, 2-calculus, proof checkers, and ZF set theory.
410  0$aLecture Notes in Computer Science,$x0302-9743 ;$v996
606   $aSoftware engineering
606   $aMathematical logic
606   $aComputer 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   $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   $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
606   $aMathematical Logic and Foundations$3https://scigraph.springernature.com/ontologies/product-market-codes/M24005
615  0$aSoftware engineering.
615  0$aMathematical logic.
615  0$aComputer logic.
615  0$aProgramming languages (Electronic computers).
615  0$aArtificial intelligence.
615 14$aSoftware Engineering/Programming and Operating Systems.
615 24$aMathematical Logic and Formal Languages.
615 24$aLogics and Meanings of Programs.
615 24$aProgramming Languages, Compilers, Interpreters.
615 24$aArtificial Intelligence.
615 24$aMathematical Logic and Foundations.
676   $a005.13/1
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$aInternational Workshop TYPES '94
906   $aBOOK
912   $a996465771703316
996   $aTypes for Proofs and Programs$9771867
997   $aUNISA