Verified Programming in Agda

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

• Ian Orton (University of Cambridge)
• Tuesday 28 February 2017, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SW01.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Education Research
• Computer Laboratory, William Gates Building, Room SW01
• Computing Education Research
• Department of Computer Science and Technology talks and seminars
• Guy Emerson's list
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.