Abstract: Structured Type Theory and the Proof Checker Agda

Catarina Coquand

Agda with the graphical interface Alfa is an interactive system for direct manipulation of proofs and programs. It is implementing Structured Type Theory which is a dependently typed functional language with modern language constructs such as pattern matching, parametrised modules and records.