703609 VU Lambda Calculus and Type Theory
summer semester 2024 | Last update: 23.01.2024 | Place course on memo listThe 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
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/
- SDG 4 - Quality education: Ensure inclusive and equitable quality education and promote lifelong learning opportunities for all.
- SDG 9 - Industry, Innovation, and Infrastructure: Build resilient infrastructure, promote inclusive and sustainable industrialization, and foster innovation.