Hauptseminar: Ausgewählte Themen im Bereich Lambdakalkül und Typen (WS 99/00)

Organisatorisches

Abweichend von den Angaben im Vorlesungsverzeichnis findet das Seminar am Freitag 11 Uhr (st!) bis 12 Uhr 30 im Raum Z1.09 in der Oettingenstr. 67 statt.

Die Termine bei den Vorträgen stimmen nicht! Der nächste Vortrag findet Freitag, den 4.2. statt. Sebastian Terwijn wird über das Goldfarb-Papier, s.u., über die Unenstscheidbarkeit der 2nd order Unifikation vortragen.

Vortragsliste

Thema I: Lambdakalkül und Beweistheorie

12.11.99 Andreas Abel

Starke Normalisierung für die Heyting-Arithmetik mit induktiven Typen,
S. 3-15 aus der Diplomarbeit von Holger Benl, Konstruktive Interpretation induktiver Definitionen, Ludwig-Maximillians-Universität, München, 1998
POSTSCRIPT

19.11.99 nicht vergeben

Starke Normalisierung fuer die Aussagenlogik zweiter Stufe
Sektionen 11.1 - 11.3 aus: Troelstra, A. S., Schwichtenberg, H., Basic Proof Theory, Cambridge University Press, Cambridge tracts in theoretical computer science, 43, 1996.
POSTSCRIPT

26.11.99 nicht vergeben

Beweisbar rekursive Funktionen der Heytings-Arithmetik zweiter Stufe
Sektionen 11.4 - 11.5 aus: Troelstra, A. S., Schwichtenberg, H., Basic Proof Theory, Cambridge University Press, Cambridge tracts in theoretical computer science, 43, 1996.
POSTSCRIPT

Thema II: Definierbarkeit und die Plotkin-Statman-Conjecture

3.12.99 nicht vergeben

Plotkin, Gordon D., Lambda-Definability in the Full Type Hierarchy, Seldin, Jonathan P., Hindley, J. Roger, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London, 1980, 363-373
ZIP

10.12.99 nicht vergeben

Jung, A., Tiuryn, J., A New Characterization of Lambda Definability, Bezem, M., Groote, J. F., Typed Lambda Calculi and Applications, Springer Verlag, Lecture Notes in Computer Science, 664, 1498, 1993, 245-257
POSTSCRIPT

17.12.99 nicht vergeben

Loader, R., The undecidability of Lambda Definibility, 199?, To appear in the Church Festschrift.
POSTSCRIPT

Thema III : Inkonsistente Typtheorien

7.1.00 Ralph Matthes

Coquand, Thierry, An Analysis of Girard's Paradox, Proceedings Symposium on Logic in Computer Science, 1986, 227-236
POSTSCRIPT

14.1.00 nicht vergeben

Coquand, Thierry, The paradox of trees in type theory, BIT, 32, 1, 1992, 10-14
POSTSCRIPT

21.1.00 nicht vergeben

Palmgren, Erik, A construction of Type: Type in Martin-Löf's Partial Type Theory with One Universe, Journal of Symbolic Logic, 56, 3, 1991, 1012-1015
POSTSCRIPT

Thema IV :(Un)Entscheidbarkeit von Unifikation und Matching höherer Ordnung

28.1.00 nicht vergeben

Huet, G., The Undecidability of Unification in Third Order Logic, Information and Control, 22, 3, April, 1973, 257-267.
ZIP

4.2.00 Sebastian Terwijn

Goldfarb, D., The Undecidability of the Second Order Unification Problem, Theoretical Computer Science, 13, 1981, 225-230.
ZIP

11.2.00 nicht vergeben

Dowek, Gilles, Third Order Matching is Decidable, Seventh Annual IEEE Symposium on Logic in Computer Science, LICS'92, IEEE, Santa Cruz, CA, USA, June, 1992, 2-10
POSTSCRIPT