Type theory is a flavour of constructive mathematics where every mathematical object is of a certain type. From this perspective, propositions become types, and their proofs become programs inhabiting their corresponding type.

Agda is a functional programming language that tastes like Haskell and features dependent types, data types that depend on values, e.g., the type of lists of a given length. Agda is not just a programming language, but also a proof assistant: it enables one to construct proofs interactively, and to use the machine to check for the correctness of their proofs.

This tutorial will serve as a brief introduction to theorem proving using the proof assistant Agda. I will introduce some common definitions and demonstrate machine assisted theorem proving at work.


Introduction to Agda



Uma Zalakain, Programming Languages Research Theme at the University of Glasgow.