|
Turing machines, Lambda calculus and proofs as programs SemesterSoSe 2023 Lecturer Hoang-Kim Nguyen Type of course (Veranstaltungsart) Seminar Contents In this seminar we will study Turing machines and the Lambda calculus, and investigate the Curry-Howard correspondence. Turing machines, introduced by Alan Turing in the 1930s, can be viewed as theoretical foundation for imperative programming languages while the Lambda calculus, introduced by Alonzo Church also in the 1930s, can be viewed as theoretical foundation of functional programming languages. As it turns out, both concepts have the same expressive power. In the first part of the seminar we will see how both give rise to partial recursive functions. Continuing with the Lambda calculus, we will study the Curry-Howard correspondence. Informally, this correspondence describes how a program can be interpreted as a proof (in constructive logic) and vice versa. This gives a direct relationship between computer programs and mathematical proofs and lies at the heart of modern proof assistants such as Coq, Lean and Agda. Literature Sorensen, Urzyczyn - Lectures on the Curry-Howard isomorphism and Pitts - Lecture notes computation theory Recommended previous knowledge Essentially none Time/Date Do 16-18 Course homepage Will be announced on my homepage (Disclaimer: Dieser Link wurde automatisch erzeugt und ist evtl. extern) Registration
BSem, MSem, LA-GySem ECTS BSem, MSem: 4,5 ECTS. LA-GySem: 6 ECTS |