Interactive Theorem Proving

• Main Course Website
• Course by Thorsten Wißmann
• Further Literature:
  • Agda Standard Library HTML Documentation
  • Programming Language Foundations in Agda
  • Verified Functional Programming in Agda (A. Stump). Verfügbar in der Universitätsbibliothek
  • Leibniz equality is isomorphic to Martin-Löf identity, parametrically (Abel, Cockx, Devriese, Timany, Wadler).
  • Let's Play Agda (Blechschmidt). Interactive Online Tutorial

Vorlesung

{-# OPTIONS --allow-unsolved-metas #-}
import Setup
import Intro
import Lists
import Decidable
import Logic
import Finite
import Sorting
import Relation
import SKI

Übungsblätter

import Blatt01
import Blatt01-SOLUTION
import Blatt02
import Blatt02-SOLUTION
import Blatt03
import Blatt03-SOLUTION
import Blatt04
import Blatt04-SOLUTION
import Blatt05
import Blatt05-SOLUTION
import Blatt06
import Blatt07

Agda Quellcode herunterladen