Lehrveranstaltungsleiter: Alexander Leitsch
Diese Lehrveranstaltung ist Wahlfach im Magisterstudium Computational Intelligence.
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.