Lehrveranstaltungsleiter: Alexander Leitsch
Diese Lehrveranstaltung ist Wahlfach im Magisterstudium Computational Intelligence (Bereich "Diskrete Mathematik und Logik").
Monday October 10, 2:00 p.m.
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.