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
Synopsis
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.
Weblinks:
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
