One main topic to be dealt with during autumn quarter is the extraction of feasible programs from constructive and classical proofs, taking advantage of the fact that this is an area of current research by our visitor for the autumn, Prof. Helmut Schwichtenberg from the University of Munich.
At this first, organizational meeting, we will make a tentative schedule and plan background expositions on topics such as realizability interpretations, suitable for student presentations.
Normalization for the typed lambda calculus, following the paper by Joachimski and Matthes. Standardization and Confluence for a Lambda Calculus with Generalized Applications.
The presentation will follow the article Buchholz, Berger, Schwichtenberg. Refined Program Extraction from Classical Proofs. Draft, 02/00.