Workshop in Termination and Type Theory

Göteborg 14-15 November 2002

EC TYPES Working Group (IST-1999-290001-TYPES)


Wednesday 13th of November

Arrival of most of the participants.
Dinner will take place at the hotel at 19.00.

Thursday 14th of November

Time Speaker Title
9.20-9.50 Andreas Abel (joint work with Ralph Matthes and Tarmo Uustalu) Generalized Iteration and Coiteration for Higher-Order Nested Datatypes
9.50-10.20 Frederic Blanqui Type Theory and Rewriting
10.20-11 Coffee break
11-11.30 David Wahlstedt A Small Language with Dependent Types, General Recursion and Size-change Termination
11.30-12 Yves Bertot Type-theoretic Functional Semantics
12-14 Lunch
14-14.30 Arne John Glenstrup Size-change Termination Principle in Partial Evaluation
14.30-15 Thorsten Altenkirch Generalized General Recursion
15-15.30 Ana Bove (joint work with Venanzio Capretta) Modelling General Recursion in Type Theory
15.30-16.10 Coffee break
16.10-16.40 Pietro Di Gianantonio (joint work with Marino Miculan) A Unifying Approach to Recursive and Co-recursive Definitions
16.40-17.10 Gilles Barthe Type-based Termination of Recursive Definitions --- The Calculus of Constructions
17.10-17.40 Venanzio Capretta General Recursion via Coinductive Types
19-21 Dinner

Friday 15th of November

Time Speaker Title
9-9.30 Paul J. Voda What Do We Gain by Integrating a Programming Language with a Theorem Prover?
9.30-10 Ulrich Berger Proving Termination by Update-induction
10-10.30 Conor McBride (joint work with James McKinna) Seeing and Doing
10.30-11.10 Coffee break
11.10-11.40 James McKinna (joint work with Conor McBride) Views for Recursion
11.40-12.10 Felix Joachimski Normalization for eta-Expansion in Pure Type Systems
12.10-14.10 Lunch
14.10-14.40 Tarmo Uustalu Recursion Schemes from Comonads a la Mendler
14.40-15.10 Klaus Aehlig Types for Finitely Iterated Inductive Definitions
15.10-15.40 Ralph Matthes Strong Normalization for Nested (Co-)Recursion
15.40-16.20 Coffee break
16.30 End of the workshop

If you have any further questions, please mail

Page last modified on November 12, 2002 by Ana Bove.