Types 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.)

• Pubblicazione: Berlin ; ; New York, : Springer, 2006
• Edizione: 1st ed. 2006.
• Descrizione fisica: 1 online resource (VIII, 280 p.)
• Disciplina: 005.131
• Soggetto topico: Automatic theorem proving; Computer programming
• Altri autori: FilliatreJean-Christophe Paulin-MohringChristine <1962-> WernerBenjamin
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: 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.
• Altri titoli varianti: TYPES 2004
• Titolo autorizzato: Types for proofs and programs
• ISBN: 3-540-31429-6
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910483584903321
• Lo trovi qui: Univ. Federico II
• Serie: Lecture notes in computer science ; ; 3839.