Types for Proofs and Programs [electronic resource] :International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers /
Contributor(s): Filliâtre, Jean-Christophe [editor.] | Paulin-Mohring, Christine [editor.] | Werner, Benjamin [editor.] | SpringerLink (Online service).Material type: BookSeries: Lecture Notes in Computer Science: 3839Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg, 2006.Description: VIII, 280 p. online resource.Content type: text Media type: computer Carrier type: online resourceISBN: 9783540314295.Subject(s): Computer science | Programming languages (Electronic computers) | Computer logic | Mathematical logic | Computer science -- Mathematics | Artificial intelligence | Computer Science | Logics and Meanings of Programs | Programming Languages, Compilers, Interpreters | Mathematical Logic and Formal Languages | Symbolic and Algebraic Manipulation | Artificial Intelligence (incl. Robotics)Online resources: Click here to access online
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.