## 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

- Introduction
- Monday 22 Nov 15:00 - 17:30, Original Completed Video
- Tuesday 23 Nov 15:00 - 16:30, Original Completed Video
- Wednesday 24 Nov 15:00 - 17:30, Original Completed Video
- Thursday 25 Nov 15:00 - 17:30, Original Completed Video

## Speaker

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

- The power of Pi., Nicolas Oury and Wouter Swierstra, 2008.
- A Brief Overview of Agda - A Functional Language with Dependent Types, Ana Bove and Peter Dybjer and Ulf Norell, 2009.
- Dependently typed programming in Agda, Ulf Norell.