SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 15:00 - 15:40 at Rebase - 14
Wed 18 Nov 2020 03:00 - 03:40 at Rebase - 14

Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution. Up to now, however, there has not been a full-scale programming language with which to experiment with these ideas. Idris 2 is a new version of the dependently typed language Idris, with a new core language based on QTT, supporting linear and dependent types. In this talk I will show the benfits of QTT in Idris 2, in particular how it improves interactive program development by reducing the search space for type-driven program synthesis; and, how resource tracking in the type system leads to type-safe concurrent programming with session types.

I am a Lecturer in Computer Science at the University of St Andrews, interested in type theory, dependently typed functional programming, compilers and metaprogramming. I am currently working on a new implementation of Idris, a dependently typed functional programming language. When I’m not doing that, you might find me playing Go (I’m about 2 kyu), walking up a hill, watching a game of cricket, or waiting for a delayed train. I’m afraid I also perpetrated the Whitespace programming language.

Tue 17 Nov
Times are displayed in time zone: Central Time (US & Canada) change

15:00 - 15:40: 14REBASE at Rebase +12h
15:00 - 15:40
Talk
REBASE
Edwin BradyUniversity of St. Andrews

Wed 18 Nov
Times are displayed in time zone: Central Time (US & Canada) change

03:00 - 03:40: 14REBASE at Rebase
03:00 - 03:40
Talk
REBASE
Edwin BradyUniversity of St. Andrews