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