02827nam 2200577 a 450 991048358490332120200520144314.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)99100000000023278020051216d2006 uy 0engurnn|008mamaatxtccrTypes for proofs and programs international workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004 : revised selected papers /Jean-Christophe Filliatre, Christine Paulin-Mohring, Benjamin Werner (eds.)1st ed. 2006.Berlin ;New York Springer20061 online resource (VIII, 280 p.) Lecture notes in computer science,0302-9743 ;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.Lecture notes in computer science ;3839.TYPES 2004Automatic theorem provingCongressesComputer programmingCongressesAutomatic theorem provingComputer programming005.131Filliatre Jean-Christophe973959Paulin-Mohring Christine1962-1751570Werner Benjamin1751571MiAaPQMiAaPQMiAaPQBOOK9910483584903321Types for proofs and programs4186561UNINA