University of Cambridge > Talks.cam > Research Students Lecture Series > Verified Programming in Agda

Verified Programming in Agda

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Mariana Marasoiu.

How do you know that a computer program does what you expect? Maybe you read the code carefully and convince yourself that it does. Maybe you go a step further and write some tests. Maybe you even get a colleague to review the code as well. All of these approaches can be useful but they are all prone to failure – subtle bugs are often missed in code reviews, and testing will almost never be exhaustive. So how can we be sure that our code is doing what it’s meant to? Agda is a programming language which allows you to prove the correctness of your programs. In this lecture I will present the basics of Agda and cover a simple example of verified programming.

This talk is part of the Research Students Lecture Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity