logo

Workshop on Proof Theory and Algorithms

23 to 29 March 2003, Edinburgh

Home | Scientific Programme & Participants | Timetable | Workshop Arrangements | Registration Form

TIMETABLE

(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
Back to ICMS Website