Abstract

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.

Talk

Introduction to Agda

Tutorial

Speaker

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

Bibliography