Interactive Theorem Proving

• Veranstaltungswebsite
• Dozent: Thorsten Wißmann
• Weitere Literatur:
• Agda Standard Library HTML Documentation
• Programming Language Foundations in Agda
• A. Stump - Verified Functional Programming in Agda (in der Universitätsbibliothek)
• Abel, Cockx, Devriese, Timany, Wadler - Leibniz equality is isomorphic to Martin-Löf identity, parametrically

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

Agda Quellcode herunterladen