TYPES 2004: Jouy-en-Josas, France

• 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