TYPES 2004: Jouy-en-Josas, France

Jean-Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner (Eds.): Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3839 Springer 2006, ISBN 3-540-31428-8 BibTeX

Robin Adams:
Formalized Metatheory with Terms Represented by an Indexed Family of Types. 1-16
Electronic Edition (link) BibTeX
Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli:
A Content Based Mathematical Search Engine: Whelp. 17-32
Electronic Edition (link) BibTeX
Gilles Barthe, Sabrina Tarento:
A Machine-Checked Formalization of the Random Oracle Model. 33-49
Electronic Edition (link) BibTeX
Stefan Berghofer:
Extracting a Normalization Algorithm in Isabelle/HOL. 50-65
Electronic Edition (link) BibTeX
Yves Bertot, Benjamin Grégoire, Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. 66-81
Electronic Edition (link) BibTeX
Ana Bove, Thierry Coquand:
Formalising Bitonic Sort in Type Theory. 82-97
Electronic Edition (link) BibTeX
Claudio Sacerdoti Coen:
A Semi-reflexive Tactic for (Sub-)Equational Reasoning. 98-114
Electronic Edition (link) BibTeX
Solange Coupet-Grimal, William Delobel:
A Uniform and Certified Approach for Two Static Analyses. 115-137
Electronic Edition (link) BibTeX
Adam Grabowski:
Solving Two Problems in General Topology Via Types. 138-153
Electronic Edition (link) BibTeX
Fredrik Lindblad, Marcin Benke:
A Tool for Automated Theorem Proving in Agda. 154-169
Electronic Edition (link) BibTeX
Lionel Elie Mamane:
Surreal Numbers in Coq. 170-185
Electronic Edition (link) BibTeX
Conor McBride, Healfdene Goguen, James McKinna:
A Few Constructions on Constructors. 186-200
Electronic Edition (link) BibTeX
Thomas Meyer, Burkhart Wolff:
Tactic-Based Optimized Compilation of Functional Programs. 201-214
Electronic Edition (link) BibTeX
Markus Michelbrink:
Interfaces as Games, Programs as Strategies. 215-231
Electronic Edition (link) BibTeX
Alexandre Miquel:
lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts. 232-251
Electronic Edition (link) BibTeX
Peter Morris, Thorsten Altenkirch, Conor McBride:
Exploring the Regular Tree Types. 252-267
Electronic Edition (link) BibTeX
Michel Parigot:
On Constructive Existence. 268-273
Electronic Edition (link) BibTeX