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.

Typed lambda calculus: normalization

Normalization for the typed lambda calculus, following the paper by Joachimski and Matthes. Standardization and Confluence for a Lambda Calculus with Generalized Applications.

Refined program extraction from classical proofs

The presentation will follow the article Buchholz, Berger, Schwichtenberg. Refined Program Extraction from Classical Proofs. Draft, 02/00.

Last modified: Thu Oct 26 09:52:32 PDT 2000