# 192.142 Introduction to Type Theories This course is in all assigned curricula part of the STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_21",{id:"j_id_21",showEffect:"fade",hideEffect:"fade",target:"isAllSteop"});});This course is in at least 1 assigned curriculum part of the 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

## Properties

• Semester hours: 2.0
• Credits: 3.0
• Type: VU Lecture and Exercise
• Format: Presence

## Learning outcomes

After successful completion of the course, students are able to

- 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.

## Subject of course

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.

## Teaching methods

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.

Oral

## Course dates

DayTimeDateLocationDescription
Wed13:00 - 15:0008.03.2023 - 28.06.2023Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed15:00 - 18:0026.04.2023Seminarraum FAV 01 C (Seminarraum 188/2) Agda install session
Introduction to Type Theories - Single appointments
DayDateTimeLocationDescription
Wed08.03.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed15.03.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed22.03.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed29.03.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed19.04.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed26.04.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed26.04.202315:00 - 18:00Seminarraum FAV 01 C (Seminarraum 188/2) Agda install session
Wed03.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed10.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed17.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed24.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed31.05.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed07.06.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed14.06.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed21.06.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories
Wed28.06.202313:00 - 15:00Seminarraum FAV 01 B (Seminarraum 187/2) Introduction to Type Theories

## Examination modalities

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.

## Course registration

Begin End Deregistration end
20.02.2023 09:00 12.03.2023 23:59 12.03.2023 23:59

## Curricula

Study CodeObligationSemesterPrecon.Info
066 931 Logic and Computation Mandatory elective
066 937 Software Engineering & Internet Computing Not specified

## Literature

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

## Previous knowledge

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)

English