LEADER 02827nam  2200577 a 450 
001 9910483584903321
005 20200520144314.0
010   $a3-540-31429-6
024 7 $a10.1007/11617990
035   $a(CKB)1000000000232780
035   $a(SSID)ssj0000320541
035   $a(PQKBManifestationID)11231115
035   $a(PQKBTitleCode)TC0000320541
035   $a(PQKBWorkID)10257813
035   $a(PQKB)10694791
035   $a(DE-He213)978-3-540-31429-5
035   $a(MiAaPQ)EBC3068270
035   $a(PPN)123130816
035   $a(EXLCZ)991000000000232780
100   $a20051216d2006      uy         0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aTypes for proofs and programs $einternational workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004 : revised selected papers /$fJean-Christophe Filliatre, Christine Paulin-Mohring, Benjamin Werner (eds.)
205   $a1st ed. 2006.
210   $aBerlin ;$aNew York $cSpringer$d2006
215   $a1 online resource (VIII, 280 p.) 
225 1 $aLecture notes in computer science,$x0302-9743 ;$v3839
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-31428-8 
320   $aIncludes bibliographical references and index.
327   $aFormalized Metatheory with Terms Represented by an Indexed Family of Types -- A Content Based Mathematical Search Engine: Whelp -- A Machine-Checked Formalization of the Random Oracle Model -- Extracting a Normalization Algorithm in Isabelle/HOL -- A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis -- Formalising Bitonic Sort in Type Theory -- A Semi-reflexive Tactic for (Sub-)Equational Reasoning -- A Uniform and Certified Approach for Two Static Analyses -- Solving Two Problems in General Topology Via Types -- A Tool for Automated Theorem Proving in Agda -- Surreal Numbers in Coq -- A Few Constructions on Constructors -- Tactic-Based Optimized Compilation of Functional Programs -- Interfaces as Games, Programs as Strategies -- ?Z: Zermelo?s Set Theory as a PTS with 4 Sorts -- Exploring the Regular Tree Types -- On Constructive Existence.
410  0$aLecture notes in computer science ;$v3839.
517 3 $aTYPES 2004
606   $aAutomatic theorem proving$vCongresses
606   $aComputer programming$vCongresses
615  0$aAutomatic theorem proving
615  0$aComputer programming
676   $a005.131
701   $aFilliatre$b Jean-Christophe$0973959
701   $aPaulin-Mohring$b Christine$f1962-$01751570
701   $aWerner$b Benjamin$01751571
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a9910483584903321
996   $aTypes for proofs and programs$94186561
997   $aUNINA