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

2.0 SE Seminar aus diskreter Mathematik und Logik (185.248, WS 2005)

Lehrveranstaltungsleiter: Alexander Leitsch

Diese Lehrveranstaltung ist Wahlfach im Magisterstudium Computational Intelligence (Bereich "Diskrete Mathematik und Logik").

First Meeting:

Monday October 10, 2:00 p.m.
Hörsaal 7,
Main Building, Karlsplatz 13


Typed Lambda Calculus and Normalization of Proofs

Proving theorems and computing functions are activities having common roots. In particular there exists a close connection between proofs in natural deduction and terms of (typed) lambda calculus; in fact there exists an isomorphism between natural deduction proofs and typed lambda terms, the so-called Curry-Howard isomorphism. In the seminar we define natural deduction, typed lambda calculus, conversions, normal forms and the Curry-Howard isomorphism. Moreover we investigate the impact of this isomorphism on the normalization of proofs. Eventually we prove the strong normalization theorem of typed lambda calculus.

Valid HTML 4.01! Viewable With Any Browser A.Leitsch