BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Agda: a practical tutorial - Matthew Daggitt
DTSTART:20181107T110000Z
DTEND:20181107T120000Z
UID:TALK114673@talks.cam.ac.uk
CONTACT:Nathanael Arkor
DESCRIPTION:Ever get the feeling that you don't quite believe your own pro
 ofs? Wouldn't it be nice if there was some infallible person always availa
 ble to check them for you? Well\, help is on hand: Agda is a dependently-t
 yped language in which you can write both classical functional programs an
 d mathematical proofs. By the Curry–Howard correspondence\, Agda is capa
 ble of deciding if your proof is correct by type-checking your Agda progra
 m. This talk will go through the basics of getting started in Agda\, provi
 de an introduction to the standard library and will involve some (dangerou
 sly) live coding.
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
END:VEVENT
END:VCALENDAR