|
Friday, 14 March 2008 |
|
| | 18:00 | - | ultimo | Pub on the Pond (info, Map (please use this link, the other links are slightly misleading)) |
| |
|
| |
Saturday, 15 March 2008 |
|
| 09:00 | - | 09:05 | Anton Setzer (Swansea) |
| | | | Opening |
| 09:05 | - | 10:05 | Michael Rathjen (Leeds) |
| | | | Universes and the limits of Martin-Löf type theory (abstract, slides) |
|
|
| 10:05 | - | 10:30 | Coffee and Tea |
|
|
| 10:30 | - | 11:10 | Peter Aczel (Manchester) |
| | | | Predicate Logic over a type setup (abstract,
slides in ps, slides in pdf, usage instructions for printing out slides) |
| 11:15 | - | 11:55 | Laura Crosilla (Florence) |
| | | | Making constructive set theory explicit (Joint work with Andrea Cantini) (abstract, slides) |
|
|
| 11:55 | - | 12:05 | Coffee and Tea |
|
|
| 12:05 | - | 12:45 | Nissim Francez (Haifa) |
| | | | Discharging sub-derivations: A proof-theoretic Curry-Howard correspondence for a λ-calculus with patterns (abstract, slides) |
| 12:45 | - | 13:15 | Roger Hindley (Swansea) |
| | | | Remarks on Bertrand Russell (informal talk) (abstract) |
|
|
| 13:15 | - | 15:00 | Lunch |
| | | | at Pub on the Pond (info, Map (please use this link, the other links are slightly misleading)) |
|
|
| 15:00 | - | 16:00 | Erik Palmgren (Uppsala) |
| | | | Type universes and ramifications (abstract, slides) |
|
|
| 16:00 | - | 16:15 | Coffee and Tea |
|
|
| 16:15 | - | 16:55 | Thorsten Altenkirch (Nottingham) |
| | | | Towards Type Theory with Continuity (abstract, slides) |
| 17:00 | - | 17:40 | Zhaohui Luo (Royal Holloway) |
| | | | LTT: a type-theoretic framework for foundational pluralism (abstract, slides) |
| 17:45 | - | 18:30 | Peter Hancock (Nottingham) |
| | | | Church encodings of ordinals, and simulation of ordinal functions (abstract, slides) |
|
|
| 19:30 | - | ultimo | Conference Dinner |
| | | | at the Bengal Brasserie (info) |
| |
|
| |
Sunday, 16 March 2008 |
|
| 09:00 | - | 10:00 | Wolfram Pohlers (Münster) |
| | | | A proof of strong normalization for intuitionistic simple type theory (abstract, slides) |
|
|
| 10:00 | - | 10:30 | Coffee and Tea |
|
|
| 10:30 | - | 11:10 | Colin Riba (INRIA Sophia Antipolis) |
| | | | Unions of Type Interpretations for Lambda-Calculus and Rewriting (abstract, slides) |
| 11:15 | - | 11:55 | William Stirton (Edinburgh) |
| | | | A sub-system of Girard's F with ordinal strength ε0 (abstract in word format, abstract in converted to pdf, slides) |
|
|
| 11:55 | - | 12:15 | Coffee and Tea |
|
|
| 12:15 | - | 12:55 | Trifon Trifonov (LMU Munich) |
| | | | Extraction from classical proofs with uniformities - a case study (abstract, slides) |
| 13:00 | - | 13:40 | Alessio Guglielmi (Bath) |
| | | | Normalisation in Deep Inference via Atomic Flows (joint work with Tom Gundersen, Bath) (abstract, slides, link to paper) |
| 13:40 | - | 13:45 | Wolfram Pohlers (Münster) |
| | | | Closing |
|
|
| 13:45 | | | Lunch |
| | | | at the Woodman (info) |
|
|
| Afternoon | Excursion |
|
|
| Evening | Dinner (Restaurant be confirmed) |
| |
| |