Idris is a general purpose functional programming language with full dependent types, building on state-of-the-art techniques in programming language research. In a dependently typed language, types are a first class language construct. Types can be parameterised by values, so that required properties of a program can be captured in the type system and verified by a type checker. This includes functional properties (does the program give the correct answer?) and extra-functional properties (does the program run within specified resource constraints?)

In this talk, I’ll introduce Idris, and show how to use types to help direct program construction. I’ll use a series of examples to show how to use it to verify realistic and important properties of software, from simple properties such as bounds verification of list functions, to more complex properties of communicating and distributed systems.

I am a Lecturer in Computer Science at the University of St Andrews, interested in type theory, dependently typed functional programming, compilers and domain specific languages (DSLs). I am currently working on the implementation of DSLs for stateful, resource-aware programming, especially for correct network protocol design and implementation, using Idris, a dependently typed functional programming language.

When I’m not doing that, you might find me playing Go (I’m about 1 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.