Idris: General Purpose Programming with Dependent Types

Speaker: Edwin Brady.

Idris (http://www.idris-lang.org/) is an experimental functional programming language with full spectrum dependent types (http://en.wikipedia.org/wiki/Dependent_type), meaning that types can be predicated on any value. Its syntax is influenced by Haskell. As well as full dependent types it supports records, type classes, tactic based theorem proving, totality checking, and an optimising compiler with a foreign function interface. One of the goals of the Idris project is to bring type-based program verification techniques to programming practitioners while still supporting efficient systems programming via an optimising compiler and interaction with external libraries.

In this talk Edwin will introduce dependently typed programming using Idris, and demonstrate its features using several examples including verified compression by run-length encoding,
management of state and side-effects and resource correctness proofs, finishing with (to the best of our knowledge!) the first ever dependently-typed arcade game...