703609 VU Lambda Calculus and Type Theory

Sommersemester 2024 | Stand: 23.01.2024 LV auf Merkliste setzen
Institut für Informatik Institut für Informatik
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
keine Angabe
Englisch
Absolventinnen und Absolventen dieses Moduls verstehen wesentliche Konzepte der Typentheorie und deren Einsatzmöglichkeit. Dies umfasst den Einsatz von Typsystemen in Programmiersprachen, den Zusammenhangen zwischen Typen und Logik, sowie den Einsatz von Typsystemen in Beweis Assistenten. Zudem haben Absolventinnen und Absolventen grundlegende Erfahrungen im praktischen Einsatz eines Beweis Assistenten erworben. Bezug zu Aurora Pilot Domains/Hubs und Interdisziplinarität. Typsysteme werden intensiv in Sprachen wie JavaScript und F# verwendet. Diese Sprachen sind von fundamentalem Interesse für eine digitale Gesellschaft, weil sie insbesondere zum Betrieb von Internet-Browsern genutzt werden, Stichwort WebAssembly. Der Curry-Howard Isomorphismus zeigt zudem auf, dass Typsysteme eine Schnittstelle zwischen mathematischer Logik und Berechnungsmodellen der Informatik bilden.

Der Kurs beinhaltet die folgenden Themen: Syntax und operationelle Semantik des ungetypten Lambda Kalküls; einfache Typentheorien; abhängige Typentheorien erster Ordnung; Formeln als Typen und Beweise als Terme; induktive Typen; polymorphe Typen; Calculus of Constructions; Coq’s Typentheorie; Metatheory von Typsystemen; Algorithmen zur Typüberprüfung; die Church-Rosser Eigenschaft; Normalisierung durch Interpretation. Zudem wird eine Einführung zum Beweisassistenten Coq gegeben, inklusive praktischer Übungen. Abschliessend geben wir eine Ausblick, wie funktionale Programmierinnen und Programmierer Typtheorie wahrnehmen, sowie auf Homotopietypentheorie.

Kombination aus Vorlesungen und Übungen

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.

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/

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/
siehe Termine
August 26 - 31, Obergurgl http://cl-informatik.uibk.ac.at/isr24/