Type-driven Development with Idris 2
- 👤 Speaker: Dr Edwin Brady - School of Computer Science, University of St Andrews
- 📅 Date & Time: Wednesday 14 May 2025, 15:05 - 15:55
- 📍 Venue: Lecture Theatre 1, Computer Laboratory, William Gates Building
Abstract
Idris is a functional programming language with first-class types, which allow properties to be expressed in the type system, and with an interactive type-driven editor which allows programs to be developed as a formal conversation with the machine. In this talk I will introduce Idris and its type system, and cover recent developments in Idris 2. In particular, I will describe how the quantities in the type system give additional expressivity which allows us to implement state machines and communicating systems and verify their properties, interactively.
Link to join virtually: https://cam-ac-uk.zoom.us/j/87421957265
A recording of this talk is available at the following link: https://www.cl.cam.ac.uk/seminars/wednesday/video/
This talk is being recorded. If you do not wish to be seen in the recording, please avoid sitting in the front three rows of 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
Series This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Chris Davis' list
- computer science
- Department of Computer Science and Technology talks and seminars
- Graduate-Seminars
- Guy Emerson's list
- Interested Talks
- Lecture Theatre 1, Computer Laboratory, William Gates Building
- Martin's interesting talks
- School of Technology
- se393's list
- Trust & Technology Initiative - interesting events
- Wednesday Seminars - Department of Computer Science and Technology
- yk449
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)

Dr Edwin Brady - School of Computer Science, University of St Andrews
Wednesday 14 May 2025, 15:05-15:55