Type-driven Development with Idris 2

Add to your list(s) Download to your calendar using vCal

• Dr Edwin Brady - School of Computer Science, University of St Andrews
• Wednesday 14 May 2025, 15:05-15:55
• Lecture Theatre 1, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Ben Karniely.

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

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

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• 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
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.