| Overview | |||
|---|---|---|---|
| Monday, 14 | Tuesday, 15 | Wednesday, 16 | |
| 8:30 | Registration | ||
| 9:00 | Topic E | Topic B | Topic A |
| 10:30 | Coffee Break | Coffee Break | Coffee Break |
| 11:00 | Topic H | Topic C | Topic F |
| 12:30 | Lunch | Lunch | Lunch |
| 14:00 | Topic D | Topic G | Topic I(*) |
| 15:30 | Coffee Break | Coffee Break | Coffee Break(*) |
| 16:00 | Industrial Panel | Brain Storming | Business Meeting(*) |
| 20:00 | APPSEM Dinner | SAS/PLILP Dinner | |
(*) shifted one hour later, as Topic I is postponed at 15:00 to avoid overlap with PLILP invited talk.
| Monday, September 14th | |
|---|---|
| 8:30 | Registration |
| 9:00 | Topic E: Automatic program transformation (N.Jones) |
| Semantics modifiers and inverse computation (Sergei Abramov, Robert Glück, 30 min) | |
| TBA (Andrej Filinski, 30 min) | |
| Specifying the semantics of program specialization using type theory (Peter Thiemann, 30 min) | |
| 10:30 | Coffee Break |
| 11:00 | Topic H: Semantics-based optimization (J.Hughes) |
| MLJ and computational lambda calculus (Nick Benton, Andrew Kennedy, 20 min) | |
| A presheaf model for polytime (Martin Hoffman, 20 min) | |
| A linear abstract machine with explicit substitution (Eike Ritter, 20 min) | |
| The TCOOL project (Martin Wehr, 20 min) | |
| 12:30 | Lunch |
| 14:00 | Topic D: Verification methods (A.Pitts, G.Rosolini) |
| Verification in SDT (Berhard Reus, 30 min) | |
| Semantics and types for the ambient calculus (Andy Gordon, 30 min) | |
| A new paradigm: call-by-observable (Paul Blain Levy, 30 min) | |
| 15:30 | Coffee Break |
| 16:00 | Industrial Panel (N.Benton, B.Thomsen) |
| Tuesday, September 15th | |
| 9:00 | Topic B: Program structuring (E.Moggi, M.Jones) |
| Program structuring in Haskell (Mark Jones, 30 min) | |
| A categorical semantics of MetaML (Eugenio Moggi, 30 min) | |
| Mutually recursive modules (Davide Ancona, 30 min) | |
| 10:30 | Coffee Break |
| 11:00 | Topic C: Integration of functional languages and proof assistants (T.Coquand, M.Mauny) |
| Transferring the ML module system to other languages (Xavier Leroy, 30 min) | |
| Module systems for proof assistants (Judicael Courant, 30 min) | |
| Type theory and functional programming (Thorsten Altenkirch, 30 min) | |
| 12:30 | Lunch |
| 14:00 | Topic G: Types and type inference in programming (E.Robinson, M.Tofte) |
| A generalization of algebraic data types (Martin Wehr, 30 min) | |
| Program analysis of ML with exceptions (Francois Pessaux, 30 min) | |
| Polymorphic type inference to solve year 2000 problems in OS/VS COBOL (Mads Tofte, 30 min) | |
| 15:30 | Coffee Break |
| 16:00 | Brain Storming (P.Dybjer) |
| 20:00 | APPSEM Dinner |
| Wednesday, September 16th | |
| 9:00 | Topic A: Semantics for object-oriented programming (P.O'Hearn) |
| TBA (Ian Stark, 30 min) | |
| A model of objects with roles (Giorgio Ghelli, 30 min) | |
| TBA (Didier Remy, 30 min) | |
| 10:30 | Coffee Break |
| 11:00 | Topic F: Games, sequentiality, and abstract machines (T.Streicher) |
| Realizability models for sequential computation (John Longley, 45 min) | |
| Control of arity in system F (Hugo Heberlin, 45 min) | |
| 12:30 | Lunch |
| 15:00 | Topic I: Domain theory and real number computation (A.Jung, A.Edalat) |
| Real Number Computation using Mobius Transformations (Abbas Edalat, 50 min) | |
| Real functions computable by finite automata (Achim Jung, 20 min) | |
| Effective and sequential definition by cases on the reals via infinite signed-digit numerals (Martin Escardo, 20 min) | |
| 16:30 | Coffee Break |
| 17:00 | Business Meeting (P.Dybjer) |