BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified Programming in Agda - Ian Orton (University of Cambridge)
DTSTART:20170228T130000Z
DTEND:20170228T140000Z
UID:TALK70908@talks.cam.ac.uk
CONTACT:Mariana Marasoiu
DESCRIPTION:How do you know that a computer program does what you expect? 
 Maybe you read the code carefully and convince yourself that it does. Mayb
 e you go a step further and write some tests. Maybe you even get a colleag
 ue to review the code as well. All of these approaches can be useful but t
 hey are all prone to failure - subtle bugs are often missed in code review
 s\, and testing will almost never be exhaustive. So how can we be sure tha
 t our code is doing what it's meant to? Agda is a programming language whi
 ch 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 pr
 ogramming.
LOCATION:Computer Laboratory\, William Gates Building\, Room SW01
END:VEVENT
END:VCALENDAR