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.
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.
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.
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.
Relevant course material:
Egbert Rijke. "Introduction to Homotopy Type Theory". Cambridge University Press, pre-publication. Available on arxiv: https://arxiv.org/abs/2212.11082
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
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
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)
