703609 VU Lambda Calculus and Type Theory

summer semester 2024 | Last update: 23.01.2024 Place course on memo list
Department of Computer Science Department of Computer Science
Prof. Dr. Herman Geuvers Prof. Dr. Herman Geuvers
Dr. Niels van der Weide Dr. Niels van der Weide
703609
VU Lambda Calculus and Type Theory
VU 2
5
Block
not applicable
English
Students who completed this course understand essential concepts of type theory and their applications. This includes the use of type systems in programming languages, the interplay of types and logic, as well as the usage of type systems for proof assistants. Students also acquired fundamental experience in the practical usage of a proof assistant. Relation to Aurora pilot domains/hubs and multidisciplinarity. Type systems are a core ingredient of programming languages such as JavaScript and F#. These languages are used to run webbrowsers (cf. WebAssembly), and are therefore highly relevant for a digital society. In the form of the Curry-Howard isomorphism it is further illustrated that type systems establish a close connection between mathematical logic and computation.

The following topics will be treated: syntax and operational semantics of
untyped lambda-calculus; simple type theory; first order dependent type
theory; formulas-as-types and proofs-as-terms; inductive types,
polymorphic types; calculus of constructions; the type theory of Coq;
simple meta theory of type systems; type checking algorithm; Church-Rosser
property; normalization property; normalization by evaluation. We will also
introduce the Coq proof assistant and allow the students to get some hands
on experience with it. Finally, we will provide a brief outlook on how
functional programmers view type theory and on homotopy type theory

combination of lectures and exercise sessions

Continuous assessment based on exercise sessions. A written test is offered at the end of the course.

Course notes will be made available to registered students.

None

The course is part of ISR 2024, the 14th International School on Rewriting, which is held from August 25 until September 1 at the Obergurgl University Center.

The course is also an Aurora Alliance (https://www.uibk.ac.at/en//international/aurora/) event.

Students of all Aurora universities (incl. Master students of the University of Innsbruck) are invited to apply for participation in this course from January 08 till January 21 at the following link (after this date, registration via the online course catalogue is possible for Innsbruck students): https://www.uibk.ac.at/en/international/aurora/aurora-course-offerings/universitat-innsbruck/

http://cl-informatik.uibk.ac.at/isr24/
see dates
August 26 - 31, Obergurgl http://cl-informatik.uibk.ac.at/isr24/