This demonstration-heavy talk looks at how programming could look, if we were to allow types to depend on terms in the language.

Watch the video


Download the presentation slides (PDF)

Useful links

Idris main website
The Idris repository 
The Idris wiki 
The trial web version of Idris


Until recently, dependent types were used for theorem provers but not for programming. What benefits can we get from combining them with regular programming?

This demo-heavy talk will demonstrate what programming could look like if we were to allow types to depend on terms in the language. Not only can we rule out more bugs than ever, but the additional type information allows for a very pleasant programming experience.

To explore this area of software, we show Idris2 and its editor experience as well as its latest features which relate type information with performance.


About the speaker

Andre Videla, University of Strathclyde

Andre Videla is a PhD student at the University of Strathclyde, focusing on Programming Languages and Type Theory. His research area is motivated by practical-use cases of software engineering and makes use of dependent types, logic, and category theory, to provide new ways to write programs that are both correct and pleasant to use. He is associated with the National Physical Laboratory.

Our events are for adults aged 16 years and over.

BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society. Join BCS today. Enjoy a 20% BCS discount on membership using BCSFACS20.

For overseas delegates who wish to attend the event, please note that BCS does not issue invitation letters.

This event is brought to you by: BCS FACS SG - Formal Aspects of Computing

Webinar: Dependent types for practical use
Date and time
Tuesday 29 March, 5:15pm - 8:00pm
This event is sold out