# Logic Seminar
Schedule

Fall quarter 2000

## Extraction of Feasible Programs

from Constructive and Classical
Proofs

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

## Schedule

**1.** Oct 10
**Typed lambda calculus: normalization.**
[JM]
(Peter Selinger)
**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.