03687nam 22007215 450 99646611470331620230221050914.03-540-31429-610.1007/11617990(CKB)1000000000232780(SSID)ssj0000320541(PQKBManifestationID)11231115(PQKBTitleCode)TC0000320541(PQKBWorkID)10257813(PQKB)10694791(DE-He213)978-3-540-31429-5(MiAaPQ)EBC3068270(PPN)123130816(EXLCZ)99100000000023278020100409d2006 u| 0engurnn|008mamaatxtccrTypes for Proofs and Programs[electronic resource] International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers /edited by Jean-Christophe Filliatre, Christine Paulin-Mohring, Benjamin Werner1st ed. 2006.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2006.1 online resource (VIII, 280 p.) Theoretical Computer Science and General Issues,2512-2029 ;3839Bibliographic Level Mode of Issuance: Monograph3-540-31428-8 Includes bibliographical references and index.Formalized 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.Theoretical Computer Science and General Issues,2512-2029 ;3839Computer scienceCompilers (Computer programs)Machine theoryComputer science—MathematicsArtificial intelligenceComputer Science Logic and Foundations of ProgrammingCompilers and InterpretersFormal Languages and Automata TheorySymbolic and Algebraic ManipulationArtificial IntelligenceComputer science.Compilers (Computer programs).Machine theory.Computer science—Mathematics.Artificial intelligence.Computer Science Logic and Foundations of Programming.Compilers and Interpreters.Formal Languages and Automata Theory.Symbolic and Algebraic Manipulation.Artificial Intelligence.005.131Filliatre Jean-Christopheedthttp://id.loc.gov/vocabulary/relators/edtPaulin-Mohring Christineedthttp://id.loc.gov/vocabulary/relators/edtWerner Benjaminedthttp://id.loc.gov/vocabulary/relators/edtBOOK996466114703316Types for Proofs and Programs771867UNISA