Russell'08 - Programme

Proof Theory Meets Type Theory

Dept. of Computer Science, Swansea University, 15/16 March 2008

Robert-Recorde Room, Faraday Building

Length of talks of invited Speakers: 45 Minutes + 15 Minutes discussion
Length of contributed talks: 30 Minutes + 10 Minutes discussion (+ 5 Minutes short break)

Friday, 14 March 2008


   18:00ultimoPub 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:05Michael Rathjen (Leeds)
Universes and the limits of Martin-Löf type theory (abstract, slides)

10:05-10:30Coffee and Tea

10:30-11:10Peter Aczel (Manchester)
Predicate Logic over a type setup (abstract, slides in ps, slides in pdf, usage instructions for printing out slides)
11:15-11:55Laura Crosilla (Florence)
Making constructive set theory explicit (Joint work with Andrea Cantini) (abstract, slides)

11:55-12:05Coffee and Tea

12:05-12:45Nissim Francez (Haifa)
Discharging sub-derivations: A proof-theoretic Curry-Howard correspondence for a λ-calculus with patterns (abstract, slides)
12:45-13:15Roger Hindley (Swansea)
Remarks on Bertrand Russell (informal talk) (abstract)

13:15-15:00Lunch
at Pub on the Pond (info, Map (please use this link, the other links are slightly misleading))

15:00-16:00Erik Palmgren (Uppsala)
Type universes and ramifications (abstract, slides)

16:00-16:15Coffee and Tea

16:15-16:55Thorsten Altenkirch (Nottingham)
Towards Type Theory with Continuity (abstract, slides)
17:00-17:40Zhaohui Luo (Royal Holloway)
LTT: a type-theoretic framework for foundational pluralism (abstract, slides)
17:45-18:30Peter Hancock (Nottingham)
Church encodings of ordinals, and simulation of ordinal functions (abstract, slides)

19:30-ultimoConference Dinner
at the Bengal Brasserie (info)

Sunday, 16 March 2008


09:00-10:00Wolfram Pohlers (Münster)
A proof of strong normalization for intuitionistic simple type theory (abstract, slides)

10:00-10:30Coffee and Tea

10:30-11:10Colin Riba (INRIA Sophia Antipolis)
Unions of Type Interpretations for Lambda-Calculus and Rewriting (abstract, slides)
11:15-11:55William 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:15Coffee and Tea

12:15-12:55Trifon Trifonov (LMU Munich)
Extraction from classical proofs with uniformities - a case study (abstract, slides)
13:00-13:40Alessio Guglielmi (Bath)
Normalisation in Deep Inference via Atomic Flows (joint work with Tom Gundersen, Bath) (abstract, slides, link to paper)
13:40-13:45Wolfram Pohlers (Münster)
Closing

13:45Lunch
at the Woodman (info)

AfternoonExcursion

EveningDinner (Restaurant be confirmed)

Anton Setzer
Last modified: Tue Apr 15 20:07:06 BST 2008