Central Library

Normal view MARC view ISBD view

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

Contributor(s): Filliatre, Jean-Christophe [editor.] | Paulin-Mohring, Christine [editor.] | Werner, Benjamin [editor.] | SpringerLink (Online service).
Material type: materialTypeLabelBookSeries: Theoretical Computer Science and General Issues: 3839Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2006Edition: 1st ed. 2006.Description: VIII, 280 p. online resource.Content type: text Media type: computer Carrier type: online resourceISBN: 9783540314295.Subject(s): Computer 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 IntelligenceAdditional physical formats: Printed edition:: No title; Printed edition:: No titleDDC classification: 004.0151 Online resources: Click here to access online
Contents:
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.
In: Springer Nature eBook
    average rating: 0.0 (0 votes)
No physical items for this record

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.

There are no comments for this item.

Log in to your account to post a comment.