Edwin Brady Tells Us What's New in Idris 2

Idris is a functional programming language with first-class types and with built-in support for interactive editing. Together, these features mean that Idris is ideally suited to "Type-driven development," where we begin by writing a type and an empty function definition, then refine the definition to a complete working program.

Recently, Edwin has been working on a new implementation, Idris 2, written in Idris itself (and now able to compile itself). In this talk, he'll give a tour of what's new in Idris 2, focusing in particular on interactive editing and type-driven development of concurrent programs.

Edwin says, "I'll aim to make the talk accessible to those with some knowledge of functional programming, but not necessarily any knowledge of type systems. At the end of the talk, I hope that you'll have a new appreciation of what types can help you do!"

Edwin is a Lecturer in Computer Science at the University of St. Andrews, interested in type theory, dependently-typed functional programming, compilers, and metaprogramming.

When he's not rewriting Idris, you might find him playing Go (he's about 2nd kyu), walking up a hill, watching a game of cricket, or waiting for a delayed train. He regrets to inform you that he is also responsible for perpetrating the Whitespace programming language.

This Meetup will be recorded and posted to YouTube. Please note that you will need to log in to Zoom with an account in order to participate and that attendance is first come, first served, limited to 100 people.