Logic Seminar Schedule
Fall quarter 2000

Here is the tentative schedule suggested by Prof. Schwichtenberg at the organizational meeting. Weekly meetings start on Tuesday, Oct. 10.

Schedule

2. Oct 17 Higher type realizability. [T1, §3.4] [T2] [BBS, §4] (Aarati Parmar)

3. Oct 24 Negative translation. [BBS, §2-3] (Matteo Slanina)

A. Oct 31 Refined program extraction from classical proofs. [BBS] (Helmut Schwichtenberg)

4. Nov 7 Non-size-increasing polynomial time computation. [H] [AS] (Bernd Finkbeiner)

5. Nov 14 Program extraction from normalization proofs. [B] (Aaron Stump)

B. Nov 21 An arithmetic for non-size-increasing polynomial time computation. [ABHS] (Helmut Schwichtenberg)

6. Nov 28 Restricting Gödel's T. [BNS] (John Goodrick)

C. Dec 5 Feasible programs from proofs. [S] (Helmut Schwichtenberg)

References

[ABHS]

Aehlig, Berger, Hofmann, Schwichtenberg. An arithmetic for non-size-increasing polynomial time computation. Preliminary draft, available from Helmut Schwichtenberg.

[AS]

Aehlig, Schwichtenberg. A syntactical analysis of non-size-increasing polynomial time computation. Proceedings of LICS'00.

[B]

Berger. Program Extraction from Normalization Proofs. TLCA'93.

[BBS]

Buchholz, Berger, Schwichtenberg. Refined Program Extraction from Classical Proofs. Draft, 02/00.

[BNS]

Bellantoni, Niggl, Schwichtenberg. Higher Type Recursion, Ramification and Polynomial Time. To appear in APAL.

[H]

Hofmann. Linear types and non-size-increasing polynomial time computation. Proceedings of LICS'99.

[JM]

Joachimski, Matthes. Short Proofs of Normalizationfor the simply-typed lambda-calculus, permutative conversions and Gödel's T. Submitted to the Archive for Mathematical Logic, 1999.

[S]

Helmut Schwichtenberg. Feasible programs from proofs. Draft 01/00.

[T1]

Troelstra. Metamathematical investigation of intuitionistic arithmetic and analysis, §3.4. Springer Lecture Notes in Mathematics 344, 1973.

[T2]

Troelstra. Article in Handbook of Proof Theory. Elsevier, 1998.