Programing with evidence

Date: Mon, Nov 22 - Thu, Nov 25 2021

Hour: 15:00

Location: BCAM and Online

Speakers: Uma Zalakain (University of Glasgow)

DATES: 22-25 November 2021 (4 sessions)
TIME: 15:00 - 17:30, except Tuesday that is from 15 to 16:30 (a total of 9:30 hours)

This course is a brief introduction to Agda, a functional programming language with dependent types. Dependent types are types that depend on values, something which, as we will see during this course, allows us to provide very detailed specifications for our programs. In fact, such is the power of dependently typed programming that it blurs the lines between computer programming and theorem proving: theorems in constructive mathematics become types in Agda, and proofs of those theorems become computable programs that inhabit their corresponding types. This correspondence enables us to completely mechanise mathematical concepts, using the machine to check the correctness of our proofs, or even to aid us in their construction.

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

*Registration is free, but mandatory before November 17th. To sign-up go to and fill the registration form.





Confirmed speakers:

Uma Zalakain (University of Glasgow)