Speaker: Bernardo Almeida (LASIGE, DI/FCUL).

Where: https://tertulia.di.fc.ul.pt/RSSmeetup.

Abstract: In this talk, we will overview Agda and see how to use it as a proof assistant. Agda is a dependently typed programming language whose powerful type system allows to specify and prove properties. Agda exploits the relation between programs and proofs, the so-called Curry-Howard correspondence, which means that we can interpret propositions as types, and proofs as programs. We will go through the book "Programming languages foundations in Agda" by Philip Wadler, Wen Kokke, and Jeremy Siek (plfa.github.io), introduce Agda and see some examples.

Bio: Bernardo Almeida is a PhD student at the Faculty of Sciences, University of Lisbon, and a student researcher at LASIGE. He received his BSc and MSc both in Computer Science, from the University of Lisbon. Currently, his main research interests are type systems and programming languages.