Workshop on Proof Theory and Algorithms
23 to 29 March 2003, Edinburgh
Home | Scientific Programme & Participants | Timetable | Workshop Arrangements | Registration FormTIMETABLE
(updated 21 March 2003)Monday | Tuesday | Wednesday | Thursday | Friday
Monday 24 March
| 0930 - 1030 | Coquand, Thierry Point-free topology and constructive mathematics |
| 1030 - 1100 | Coffee break |
| 1100 - 1200 | Berger, Ulrich Uniform Heyting Arithmetic as a common framework for constructive and classical mathematics |
| 1200 - 1300 | Schwichtenberg, Helmut Program extraction from classical proofs |
| 1300 - 1430 | Lunch break |
| 1430 - 1530 | Oliva, Paulo On the extraction of polynomial-time algorithms from ineffective proofs in feasible analysis |
| 1530 - 1630 | Berardi, Stefano An intuitionistic model of Delta Zero Two |
| 1630 - 1700 | Tea/coffee break |
| 1700 - 1800 | Mints, Grigori Dynamical topological logic |
| 1800 | Wine Reception |
Monday | Tuesday | Wednesday | Thursday | Friday
Tuesday 25 March
| 0930 - 1030 | Avigad, Jeremy Hilbert spaces and subsystems of analysis |
| 1030 - 1100 | Coffee break |
| 1100 - 1200 | Kohlenbach, Ulrich Proof theoretic applications to functional analysis |
| 1200 - 1300 | Leustean, Laurentiu Proof mining in fixed point theory |
| 1300 - 1430 | Lunch break |
| 1430 - 1530 | Hofmann, Martin A new deductive system for Kozen's mu-calculus |
| 1530 - 1630 | Hernest, Dan A complexity analysis of functional interpretations |
| 1630 - 1700 | Tea/coffee break |
| 1700 - 1800 | Baaz, Matthias Proof analysis by resolution |
| 1800 | Discussion |
Monday | Tuesday | Wednesday | Thursday | Friday
Wednesday 26 March
| 0930 - 1030 | Krivine, Jean-Louis Realizing dependent choice in classical logic |
| 1030 - 1100 | Coffee break |
| 1100 - 1200 | Danos, Vincent Disjunctive normal forms and multi-exception handlers |
| 1200 - 1300 | Matthes, Ralph Programs with nested datatypes from proofs |
| 1300 - 1430 | Lunch break |
| 1430 - 1530 | Tupailo, Sergei On the intuitionistic strength of monotone inductive definitions |
| 1530 - 1630 | Setzer, Anton Monotone inductive definitions on families of sets |
| 1630 - 1700 | Tea/coffee break |
| 1700 - 1800 | Laurent, Olivier Classical isomorphisms of types and the real exponential field |
| 1800 - 1900 | Hirschowitz, Michel Abstract games |
Monday | Tuesday | Wednesday | Thursday | Friday
Thursday 27 March - (note different pm)
| 0930 - 1030 | Lombardi, Henri Finding a constructive content for some proofs in abstract algebra |
| 1030 - 1100 | Coffee break |
| 1100 - 1200 | Carbone, Alessandra Computations in groups and formal proofs |
| 1200 - 1300 | Grisi de Oliveiera, Anjolina Sequentialization and splitting theorems for proof graphs |
| 1300 - 1400 | Lunch break |
| 1400 - 1500 | Robinson, Edmund Proof nets for classical logic |
| 1500 - 1600 | Fuhrmann, Carsten An order-enriched view of the classical sequent calculus |
| 1600 - 1630 | Tea/coffee break |
Monday | Tuesday | Wednesday | Thursday | Friday
Friday 28 March
| 0930 - 1030 | Urban, Christian Nominal unification |
| 1030 - 1100 | Coffee break |
| 1100 - 1200 | Curien, Pierre-Louis Introduction to ludics |
| 1200 - 1300 | Faggian, Claudia Ludics: dynamics and interactive observability |
| 1300 - 1430 | Lunch break |
| 1430 - 1530 | Streicher, Thomas A universal model for infinitary lambda calculus with errors |
| 1530 - 1630 | Ehrhard, Thomas Semantics and syntax of the differential lambda-calculus |
| 1630 - 1700 | Tea/coffee break |
| 1700 | Discussion |
Monday | Tuesday | Wednesday | Thursday | Friday
Home | Scientific Programme & Participants | Timetable | Workshop Arrangements | Registration Form