TYPES 2004 conference
December 15-18, 2004

Campus Thalès
67, rue Charles de Gaulle - 78350 Jouy-en-Josas - FRANCE

Introduction

Registration
How to get to Campus Thalès
Social event

Submit a talk
Invited speakers
Programme
List of participants

Organising committee

Related events
History

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 co-recursive functions in the calculus of inductive constructions (slides)
Yves Bertot (INRIA Sophia-Antipolis)
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 E-bicategory of E-categories (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 First-Order Data Types and Size-Change 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 Proof-Carrying 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)

FOL-nabla 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 Sophia-Antipolis), Arnaud Spiwack (ENS Cachan)
Interfaces as games, programs as strategies (slides)
Markus Michelbrink (University of Swansea)
A machine-checker formalization of the generic model and the random oracle model (slides)
Sabrina Tarento, Gilles Barthe (INRIA Sophia-Antipolis)
Verification of BDD-Algorithms 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)
First-order 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 first-order 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 Martin-Lö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 Cruz-Filipe ( 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 simply-typed Lambda-calculus (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