[ Lehrveranstaltungen 185/2 ]
[ AG Theoretische Informatik und Logik ]
[ Fachbereich Informatik ]
[ Technische Universität Wien ]

## Seminar in Logic (185.318)

Lehrveranstaltungsleiter:
Alexander Leitsch

Diese Lehrveranstaltung ist Wahlfach im Magisterstudium *Computational Intelligence*.

**First Meeting:**

Tuesday, October 11 2010, 14:00

Seminar Room Gödel

Favoritenstrasse 9, ground floor

**CONTENT:**
** Proofs and Types**

Typed Lambda calculus is a strong formalism for representing and analyzing formal proofs and for programming. In this seminar we investigate first the relation between natural deduction and typed Lambda calculus (the Curry-Howard isomorphism) and prove the strong normalization theorem for typed Lambda calculus. Gödel's system T and Girard's system F are introduced and strong normalization for F is proved. Finally we focus on the representability of computable functions in T and F.

**Time and Place:** Tuesday 14-16, Seminar Room Gödel.

**Material: J.Y. Girard, P. Taylor, Y. Lafont. Proofs and Types. Cambridge University Press**

**Requirements:** firm background in logic and Lambda-calculus, basic knowledge in type theory is desirable.

A.Leitsch