TUTORIAL: Idris - Practical Software Verification with Dependent Types

Idris is a general purpose functional programming language with full dependent types, building on state-of-the-art techniques in programming language research. Dependent types allow types to be predicated on any value - in this way, required properties of a program can be captured in the type system, and verified by a type checker. This includes functional properties (i.e. does the program give the correct answer) and extra-functional properties (i.e. does the program run within specified resource constraints).

Idris aims to bring type-based program verification techniques to programming practitioners while supporting efficient systems programming via an optimising compiler and interaction with external libraries.

In this tutorial, I will use a series of examples to show how dependent types may be used for verifying realistic and important properties of software, from simple properties such as array bounds verification, to more complex properties of communicating and distributed systems.

Tutorial objectives:

The main objective of the tutorial is to give an overview of what is expressible in modern, state-of-the-art, type systems, and to give participants some introductory experience with the Idris programming language.

The tutorial will explain why software correctness, particularly extra-functional correctness, is important, and show how Idris' dependent type system can support this. It will cover:

• Getting started: compiling and running programs
• Simple functional properties of lists
• Extra-functional properties including side-effects and resource usage protocols
• A concluding example: using the type system to reason about communicating systems

By the end of the tutorial, participants will understand how to express invariants in a dependent type system, how to write programs which respect those invariants, and how to use embedded domain specific languages as an abstraction layer over those invariants to reduce or even eliminate the theorem proving burden on application developers.

Code for the tutorial examples will be made available, along with accompanying exercises.

Target audience:

Participants should be comfortable reading (but not necessarily writing) a typed functional language such as Haskell or OCaml. No advance knowledge of dependent types or software verification will be required.

Participants should install Idris on a laptop beforehand to follow along with examples (instructions at http://idris-lang.org/download).

Verifying Stateful and Side-effecting Programs using Dependent Types

Dependent types allow us to express a program's behaviour precisely in its type, meaning that type checking is equivalent to formally and mechanically checking a program's correctness. Introductory examples typically involve length preserving operations on lists, or ordering invariants on sorting. Realistically, though, programming is not so simple: programs interact with users, communicate over networks, manipulate state, deal with erroneous input, and so on. In this talk I will show how advanced type systems allow us to express such interactions precisely, and how they support verification of stateful systems as a result. As examples, I will show simple communication protocols, and a word game (Hangman), in the Idris programming language.

Talk objectives: I aim to show that, with a sufficiently expressive type system, writing a correct program ought to be easier than writing an incorrect program!

Target audience: Developers interested in type systems, software correctness, or programming language research in general. Some ability to read (but not necessarily write) a functional language such as Haskell or OCaml will be assumed.