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). Available in the university library
  • Leibniz equality is isomorphic to Martin-Löf identity, parametrically (Abel, Cockx, Devriese, Timany, Wadler).
  • Let's Play Agda (Blechschmidt). Interactive Online Tutorial

Lectures

{-# OPTIONS --allow-unsolved-metas --guardedness #-}
import Setup
import Intro
import Lists
import Decidable
import Logic
import Finite
import Sorting
import Relation
import SKI
import SKIx
import Partial
import Coinduction
import Undecidable

Exercise Sheets

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 Blatt06-SOLUTION
import Blatt07
import Blatt07-SOLUTION
import Blatt08
import Blatt08-SOLUTION

Agda Quellcode herunterladen