Programing with evidence

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)
LOCATION: BCAM and Online

ABSTRACT:
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.


REFERENCES:
A Brief Overview of Agda - A Functional Language with Dependent Types, Ana Bove and Peter Dybjer and Ulf Norell, https://doi.org/10.1007/978-3-642-03359-9_6
Dependently typed programming in Agda, Ulf Norell, https://doi.org/10.1145/1481861.1481862
The power of Pi, Nicolas Oury and Wouter Swierstra, https://doi.org/10.1145/1411204.1411213
Prerequisites:


*Registration is free, but mandatory before November 17th. To sign-up go to https://forms.gle/qoMBafSGhhHNcXwg7 and fill the registration form.

• BCAM-Course_20211122