Types for Proofs and Programs International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers
by
Filliâtre, Jean-Christophe. editor.
Title
:
Types for Proofs and Programs International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers
Author
:
Filliâtre, Jean-Christophe. editor.
ISBN
:
9783540314295
Physical Description
:
VIII, 280 p. online resource.
Series
:
Lecture Notes in Computer Science, 3839
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.
Subject Term
:
Computer science.
Logic design.
Algebra -- Data processing.
Artificial intelligence.
Logics and Meanings of Programs.
Programming Languages, Compilers, Interpreters.
Mathematical Logic and Formal Languages.
Symbolic and Algebraic Manipulation.
Artificial Intelligence (incl. Robotics).
Added Author
:
Filliâtre, Jean-Christophe.
Paulin-Mohring, Christine.
Werner, Benjamin.
Added Corporate Author
:
SpringerLink (Online service)
Electronic Access
:
Library | Material Type | Item Barcode | Shelf Number | Status |
---|
IYTE Library | E-Book | 509921-1001 | QA76.9 .L63 | Online Springer |