|
|
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
|
