# 192.142 Introduction to Type Theories Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_21",{id:"j_id_21",showEffect:"fade",hideEffect:"fade",target:"isAllSteop"});});Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_23",{id:"j_id_23",showEffect:"fade",hideEffect:"fade",target:"isAnySteop"});}); 2023S

2023S, VU, 2.0h, 3.0EC

## Merkmale

• Semesterwochenstunden: 2.0
• ECTS: 3.0
• Typ: VU Vorlesung mit Übung
• Format der Abhaltung: Präsenz

## Lernergebnisse

Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage

- identify and understand the rules of type theories, in particular Martin-Löf Type Theory and Calculus of Inductive Constructions,

- apply the rules to derive judgments in type theories

- formally prove theorems about properties of software data structures and mathematical structures in proof assistants (Agda and Coq),

- understand and explain the main differences between different type theories,

- reason about meta-theoretic properties of type theories.

## Inhalt der Lehrveranstaltung

Proofs of software correctness are usually long, technical and involved, which reduces our confidence they are indeed correct. A similar issue, that proofs are not accepted by the community, is present in mathematics if the proofs are too long or involve computer programs in proof construction.

Proof assistants are computer systems that allow a user to formally verify their proofs and thus avoid errors in the deduction. There are several proof assistants in use and a vast majority of them is based on mathematical foundations called type theories. In order to understand and develop proof constructions in proof assistants, one needs to understand the type theories behind them: what are their syntactic components, inference rules, and derivations, and how to use them in proof development.

The focus of this course is on the mathematical foundation itself and not only on the tools used in formalizations. The course is divided in five parts/topics:

1) Martin-Löf type theory (MLTT) - where we will describe the most common dependent types and ingredients of type theories.

2) Agda (proof assistant based on MLTT) - where we will get to know how to use MLTT to formalize proofs.

3) Calculus of inductive constructions (CIC) - where we will describe the differences and nuances between different type theories.

4) Coq (proof assistant based on CIC) - where we will get to know how to use CIC to formalize proofs in the most commonly used proof assistant.

5) Meta-theory of type theories -  where we will formally define a type theory and relate it to first-order and other higher-order theories.

## Methoden

The course material, especially on topics 1, 3, and 5, will follow seminal books in the area (see list below). In addition, lecture notes about using proof assistant will be distributed online, at the beginning of each lecture.

There will be a total of 5 homework problem sets. The 4 performances on the 5 problem sets will count towards the final course grade. After each part/topic of the course, a homework will be available on TUWEL.The students will have 2 weeks to complete the homework.The homework solutions are individual work of each student and will be marked as such. Collaboration between students on homework solutions is not permitted. The students are allowed to use all resources they can find.

In case of questions about course material or homework problems, students are advised to talk to the course staff as soon as possible. The course team is committed and happy to help students, during office hours and even beyond.

Mündlich

## LVA Termine

TagZeitDatumOrtBeschreibung
Mi.13:00 - 15:0008.03.2023 - 28.06.2023Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.15:00 - 18:0026.04.2023Seminarraum FAV 01 C (Seminarraum 188/2) Agda install session
Introduction to Type Theories - Einzeltermine
TagDatumZeitOrtBeschreibung
Mi.08.03.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.15.03.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.22.03.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.29.03.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.19.04.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.26.04.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.26.04.202315:00 - 18:00Seminarraum FAV 01 C (Seminarraum 188/2) Agda install session
Mi.03.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.10.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.17.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.24.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.31.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.07.06.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.14.06.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.21.06.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Mi.28.06.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories

## Leistungsnachweis

The course grade will be based on homework solutions and an oral exam.

A homework is considered successfully completed if it is submitted on time and it was marked with at least 50% of the points. After successfully completing at least 4 homeworks, students can apply for an oral examination. The average of the best 4 out of 5 homework solutions will represent the basis for the grade in the oral exam.

At the oral exam, students will discuss and defend their homework solutions and answer questions about the overall course material.

## LVA-Anmeldung

Von Bis Abmeldung bis
20.02.2023 09:00 12.03.2023 23:59 12.03.2023 23:59

## Curricula

StudienkennzahlVerbindlichkeitSemesterAnm.Bed.Info
066 931 Logic and Computation Gebundenes Wahlfach
066 937 Software Engineering & Internet Computing Keine Angabe

## Literatur

Relevant course material:

• For topic 1, we will follow the presentation of Martin-Löf type theory from the first chapter of following book:

Egbert Rijke. "Introduction to Homotopy Type Theory". Cambridge University Press, pre-publication. Available on arxiv: https://arxiv.org/abs/2212.11082

• For topic 3, we will follow:

Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. Bruno Woltzenlogel Paleo; David Delahaye. All about Proofs, Proofs for All, 55, College Publications, 2015, Studies in Logic (Mathematical logic and foundations), 978-1-84890-166-7. hal-01094195f

• For topic 5, we will follow:

Haselwarter, P. G. and Bauer, A., “Finitary type theories with and without contexts”, arXiv e-prints arXiv:2112.00539, 2021.

Petković Komel, Anja, "Meta-analysis of type theories with an application to the design of formal proofs", PhD thesis. University of Ljubljana, 2021. Available at URL: https://anjapetkovic.com/img/doctoralThesis.pdf

Haselwarter, Philipp Georg, 2022, Effective metatheory for type theory. PhD thesis. University of Ljubljana. Available at URL: https://repozitorij.uni-lj.si/IzpisGradiva.php?lang=eng&id=134439

## Vorkenntnisse

The course is recommended for master students and PhD students in Computer Science and Mathematics.

Familiarity with first-order logic will be assumed, as well as basic knowledge of programming. Any experience with proof assistants (Coq, Agda, Lean, Isabelle) is beneficial, but not mandatory. The course is self-contained.

Equipment: A computer with either Linux, IOS/macOS or Windows.

* not a tablet nor a smartphone

* virtual OS is possible (e.g. VirtualBox)

Englisch