LEADER 04180nam  22007935  450 
001 9910483766003321
005 20251226200542.0
010   $a3-540-74464-9
024 7 $a10.1007/978-3-540-74464-1
035   $a(CKB)1000000000491057
035   $a(SSID)ssj0000320542
035   $a(PQKBManifestationID)11232594
035   $a(PQKBTitleCode)TC0000320542
035   $a(PQKBWorkID)10249568
035   $a(PQKB)10477343
035   $a(DE-He213)978-3-540-74464-1
035   $a(MiAaPQ)EBC3067581
035   $a(PPN)123164532
035   $a(MiAaPQ)EBC336945
035   $a(BIP)34164985
035   $a(BIP)14496008
035   $a(EXLCZ)991000000000491057
100   $a20100301d2007      u|         0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aTypes for Proofs and Programs $eInternational Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers /$fedited by Thorsten Altenkirch, Conor McBride
205   $a1st ed. 2007.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2007.
215   $a1 online resource (VIII, 272 p.) 
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4502
300   $aBibliographic Level Mode of Issuance: Monograph
311 08$a3-540-74463-0 
320   $aIncludes bibliographical references and index.
327   $aWeyl?s Predicative Classical Mathematics as a Logic-Enriched Type Theory -- Crafting a Proof Assistant -- On Constructive Cut Admissibility in Deduction Modulo -- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond -- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq -- Deciding Equality in the Constructor Theory -- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family -- Truth Values Algebras and Proof Normalization -- Curry-Style Types for Nominal Terms -- (In)consistency of Extensions of Higher Order Logic and Type Theory -- Constructive Type Classes in Isabelle -- Zermelo?s Well-Ordering Theorem in Type Theory -- A Finite First-Order Theory of Classes -- Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers -- Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs -- Subset Coercions in Coq -- A Certified Distributed Security Logic for Authorizing Code.
330   $aThe refereed post-proceedings of the International Workshop of the Types Working Group are presented in this volume. The 17 papers address all current issues in formal reasoning and computer programming based on type theory, including languages and computerized tools for reasoning; applications in several domains, such as analysis of programming languages; certified software; formalization of mathematics; and mathematics education.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4502
606   $aCompilers (Computer programs)
606   $aComputer science
606   $aMachine theory
606   $aComputer science$xMathematics
606   $aArtificial intelligence
606   $aCompilers and Interpreters
606   $aComputer Science Logic and Foundations of Programming
606   $aFormal Languages and Automata Theory
606   $aSymbolic and Algebraic Manipulation
606   $aArtificial Intelligence
615  0$aCompilers (Computer programs).
615  0$aComputer science.
615  0$aMachine theory.
615  0$aComputer science$xMathematics.
615  0$aArtificial intelligence.
615 14$aCompilers and Interpreters.
615 24$aComputer Science Logic and Foundations of Programming.
615 24$aFormal Languages and Automata Theory.
615 24$aSymbolic and Algebraic Manipulation.
615 24$aArtificial Intelligence.
676   $a005.13
701   $aAltenkirch$b Thorsten$f1962-$0930976
701   $aMcBride$b Conor$01756812
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a9910483766003321
996   $aTypes for proofs and programs$94194336
997   $aUNINA