[ 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.

Valid HTML 4.01! Viewable With Any Browser A.Leitsch