FEEDBACK Smiley face
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 /

Contributor(s): Filliâtre, Jean-Christophe [editor.] | Paulin-Mohring, Christine [editor.] | Werner, Benjamin [editor.] | SpringerLink (Online service).
Material type: materialTypeLabelBookSeries: 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
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 eBooks
Tags from this library: No tags from this library for this title. Add tag(s)
Log in to add tags.
    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.

© IIIT-Delhi, 2013 | Phone: +91-11-26907510| FAX +91-11-26907405 | E-mail: library@iiitd.ac.in