Die Folien der Veranstaltung werden in zwei Versionen bereitgestellt. Die normalen ps und pdf Files enthalten eine Druckversion der Folien ohne eventuell benutzte "Animationen". Das anim file enthält die vollständige PDF Version mit Animationen.
| Einführung | Automatisierte Logik | |
| Teil I: Formalisierung | ||
| Einheit 2: | Grundkonzepte formaler Kalküle | |
| Einheit 3: | Refinement Logic | |
| Einheit 4: | Interaktive Beweisführung | |
| Einheit 5: | Lambda-Kalkül | |
| Einheit 6: | Die einfache Typentheorie | |
| Einheit 7: | Abhängige Datentypen | |
| Teil II: Konstruktive Typentheorie | ||
| Einheit 8: | Systematik des Aufbaus formaler Theorien | |
| Einheit 9: | Logik und Programmierung in der Typentheorie | |
| Einheit 10: | Fortgeschrittene Konzepte der CTT | |
| Teil III: Automatisierung des formalen Schliessens | ||
| Teil IV: Programmsynthese | ||