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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Verified Programming in Agda

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

MRC Cognition & Brain Sciences Unit, 15 Chaucer Road, Cambridge CB2 7EF Average on weekdays: 8929.31774809 kWh The Nightingale Room, Peterhouse

Other talks

Talk TBC Title to be confirmed Online Causal Inference Seminar CSAR lecture: 46&: Development of a probiotic that supports the natural removal of forever chemicals from the body Online Causal Inference Seminar Theophilus Richmond’s The First Crossing: The Transition from Slavery to Indentureship in the Caribbean and the Case of the Black Slave on the Hesperus
 

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