Interactive Theorem Proving
===========================

* [Veranstaltungswebsite](https://www8.cs.fau.de/teaching/ss26/interactive-theorem-proving-sose-2026/)
* Dozent: [Thorsten Wißmann](https://thorsten-wissmann.de)
* Weitere Literatur:
  - [Agda Standard Library HTML Documentation](https://agda.github.io/agda-stdlib/v2.3/)
  - [Programming Language Foundations in Agda](https://plfa.inf.ed.ac.uk/)
  - [A. Stump - Verified Functional Programming in Agda](https://dl.acm.org/doi/book/10.1145/2841316) (in der Universitätsbibliothek)
  - [Abel, Cockx, Devriese, Timany, Wadler - Leibniz equality is isomorphic to Martin-Löf identity, parametrically](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/leibniz-equality-is-isomorphic-to-martinlof-identity-parametrically/50D76A9C314AB24E7CD46DA4A0A766EB)

Vorlesung
---------

```
{-# OPTIONS --allow-unsolved-metas #-}
import Setup
import Intro
import Lists
import Decidable
import Logic
import Finite
```

Übungsblätter
-------------
```
import Blatt01
import Blatt01-SOLUTION
import Blatt02
import Blatt02-SOLUTION
import Blatt03
import Blatt03-SOLUTION
import Blatt04
```

<div style="display: none;">
</div>