BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Type-driven Development with Idris 2 - Dr Edwin Brady - School of 
 Computer Science\, University of St Andrews
DTSTART:20250514T140500Z
DTEND:20250514T145500Z
UID:TALK223327@talks.cam.ac.uk
CONTACT:Ben Karniely
DESCRIPTION:Idris is a functional programming language with first-class ty
 pes\, which allow properties to be expressed in the type system\, and with
  an interactive type-driven editor which allows programs to be developed a
 s a formal conversation with the machine.  In this talk I will introduce I
 dris and its type system\, and cover recent developments in Idris 2. In pa
 rticular\, I will describe how the quantities in the type system give addi
 tional expressivity which allows us to implement state machines and commun
 icating systems and verify their properties\, interactively.\n\nLink to jo
 in virtually: https://cam-ac-uk.zoom.us/j/87421957265\n\nA recording of th
 is talk is available at the following link: https://www.cl.cam.ac.uk/semin
 ars/wednesday/video/\n\nThis talk is being recorded. If you do not wish to
  be seen in the recording\, please avoid sitting in the front three rows o
 f seats in the lecture theatre. Any questions asked will also be included 
 in the recording. The recording will be made available on the Department
 ’s webpage
LOCATION:Lecture Theatre 1\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR