
Tentative Programme
Due to the large number of talk submissions, all submitted talks are
planned to be of 15mn plus 5mn for questions.
Wednesday 15 December 2004
09:00 Coffee
10:20 Opening
10:30 Session W1
 Mathematics in type theory (slides)
 Zhaohui Luo (Royal Holloway, University of London)
 Codata (slides)
 Thorsten Altenkirch (University of Nottingham)
 Partial corecursive functions in the calculus of inductive constructions (slides)
 Yves Bertot (INRIA SophiaAntipolis)
 Truly nested datatypes through dependent datatypes  a challenge for Coq (slides)
 Ralph Matthes (LMU München)
 Standard Equipment for Inductive Datatypes
 Conor McBride (Royal Holloway, University of London)
12:10 Lunch
14:10 Session W2
 An Ebicategory of Ecategories (slides)
 Olov Wilander (University of Uppsala)
 Pointfree Integration Theory without Choice (slides)
 Bas Spitters (Nijmegen University)
 Relative formal topology
 Maria Emilia Maietti, Silvio Valentini (University of Padova)
 Mapping the Classical Type Theory of Farmer's STTWU into the Constructive Type Theory of COQ (slides)
 Freek Wiedijk (Nijmegen University)
15:30 Break
16:00 Session W3
 Type Theory with FirstOrder Data Types and SizeChange Termination (slides)
 David Wahlstedt (Chalmers University)
 Polymorphism in type theory
 Johan Georg Granström (University of Uppsala)
 Interactive algebra course with formalised proofs and definitions (slides)
 Iris Loeb, Lionel Elie Mamane (Nijmegen University), Herman Geuvers (Nijmegen University)
 Coherence and Confluence
 Zoran Petric (University of Novi Sad), Kosta Došen (SANU, Belgrade)
17:20 Break
17:50 Demo session
 Proof General / Eclipse  A generic interface for interactive theorem provers
 Daniel Winterstein (University of Edinburgh) [presentation by Lucas Dixon (University of Edinburgh)]
18:10 Plain presentation of the posters
 A Modular Lattice Library to Develop Certified Terminating Static Analyses (slides)
 David Pichardie (IRISA)
 Automatizing geometry using Coq (slides)
 Julien Narboux (INRIA Futurs)
18:20 Parallel presentation of the posters
18:50 End
Thursday 16 December 2004
09:00 Invited talk
 The Essence of ProofCarrying Code
 Zhong Shao (Yale University)
10:00 Session T1
 A Dependent Type Theory with Names and Binding (slides)
 Ulrich Schoepp, Ian Stark (University of Edinburgh)
10:20 Break
10:50 Session T1 (continued)
 FOLnabla in Higher Order Abstract Syntax (slides)
 Marino Miculan, Ivan Scagnetto (University of Udine)
 Higher Order Datatypes Via Containers (slides)
 Neil Ghani (Leicester University), Thorsten Altenkirch (University of Nottingham), Tarmo Uustalu (IoC Tallinn), Michael Abbott (Leicester University)
 A proof search specification of the pi calculus (slides)
 Alwen Tiu, Dale Miller (INRIA Futurs)
 Signals and comonads (slides)
 Tarmo Uustalu, Varmo Vene (IoC Tallinn)
12:10 Lunch
14:10 Session T2
 Functional Method (slides)
 Luigi Liquori (INRIA SophiaAntipolis), Arnaud Spiwack (ENS Cachan)
 Interfaces as games, programs as strategies (slides)
 Markus Michelbrink (University of Swansea)
 A machinechecker formalization of the generic model and the random oracle model (slides)
 Sabrina Tarento, Gilles Barthe (INRIA SophiaAntipolis)
 Verification of BDDAlgorithms in Isabelle/HOL (slides)
 Veronika Ortner, Norbert Schirmer (TU München)
15:30 Break
16:00 Session T3
 Formalising Bitonic Sort (slides)
 Ana Bove, Thierry Coquand (Chalmers University)
 Proof by contextual menu
 Christophe Raffalli (Savoie University)
 Overloading in Agda (slides)
 Catarina Coquand (Chalmers University)
 Efficient Type Based Parsing in Strict Languages (slides)
 Claudio Sacerdoti Coen (INRIA Futurs), Stefano Zacchiroli (Bologna)
17:20 End
Visit and reception at Château de Breteuil
Friday 17 December 2004
09:00 Invited talk
 Toward a formal proof of the Kepler Conjecture (slides)
 Tom Hales (Pittsburgh University)
10:00 Session F1
 Proving Bounds for Real Linear Programs in Isabelle/HOL (slides)
 Steven Obua (TU München)
10:20 Break
10:50 Session F1 (continued)
 Verifying inequalities over real numbers in Coq (slides)
 Roland Zumkeller (INRIA Futurs)
 Formalising Lagrange Theorem in Coq (slides)
 Dan Synek (Nijmegen University)
 Surreal Numbers in Coq (slides)
 Lionel Elie Mamane (Nijmegen University)
 Subsets in formalised linear algebra (slides)
 Jasper Stein (Nijmegen University)
12:10 Lunch
14:10 Session F2
 The Four Color Theorem in Coq
 Georges Gonthier (Microsoft Research Cambridge)
 IsaPlanner: A proof planning framework for Isabelle (slides)
 Lucas Dixon (University of Edinburgh)
 Firstorder reasoning in the calculus of inductive constructions
 Pierre Corbineau (University Paris Sud)
 Geometric Logic and Proof Objects (slides)
 Marc Bezem (Bergen University)
15:30 Break
16:00 Session F3
 A Formalisation of the Metatheory of Pure Type Systems in Coq (slides)
 Robin Adams (University of Manchester)
 Porting Proofs Between HOL Implementations (slides)
 Sebastian Skalberg (TU München)
 A Quantifier Elimination Procedure over ACFs in Coq using Maple (slides)
 Micaela Mayero (University Paris 13), David Delahaye (CNAM)
17:00 Break
17:30 Plain demo session
 An overview of the MRG project (slides)
 Lennart Beringer
 PhoX
 Christophe Raffalli (Savoie University)
 A reflexive tactic for firstorder reasoning in Coq
 Pierre Corbineau (University Paris Sud)
 Epigram
 Conor McBride (Royal Holloway, University of London)
18:50 End
Business meeting after dinner
Saturday 18 December 2004
09:00 Invited talk
 100 years of Zermelo's axiom of choice: what was the problem with it?
 Per MartinLöf (Stockholm University)
10:00 Session S1
 Type Setups for predicate logic (slides)
 Peter Aczel (University of Manchester)
10:20 Break
10:50 Session S1 (continued)
 Semantical Cut Elimination in Intuitionistic Deduction Modulo (slides)
 Olivier Hermant (INRIA Futurs)
 On constructive existence
 Michel Parigot (CNRS, University Paris 7)
 A cut elimination theorem for set theory (slides)
 Gilles Dowek (INRIA Futurs), Alexandre Miquel (University Paris 7)
 Continuations, Backtracking and Limits: A Notion of Construction for Classical Logic (slides)
 Stefano Berardi (University of Torino)
12:10 Lunch
13:30 Session S2
 A logical model for explicit operators (slides)
 Delia Kesner, Stéphane Lengrand (University Paris 7) (University Paris 7)
 Executing Extracted Programs (slides)
 Luís CruzFilipe ( University of Lisbon), Pierre Letouzey (LMU München)
 Program extraction in constructive analysis
 Helmut Schwichtenberg (LMU München)
 Extracting a normalization algorithm from a proof of weak normalization for the simplytyped Lambdacalculus (slides)
 Stefan Berghofer (TU München)
14:50 Break
15:00 Session S3
 Arguments for a minimal type theory (slides)
 Giovanni Sambin (University of Padova)
 Declarative Language Definitions and Code Generation by Linearization (slides)
 Aarne Ranta (Chalmers University)
 Building Multimodal Dialogue Systems in GF (slides)
 Björn Bringert (Chalmers University)
 Towards a translation of Weak Type Theory into Dependent Type Theory (slides)
 Georgi Jojgov (Eindhoven University)
16:20 End
