Idris

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.

See the Idris site for further details.

Contact: Edwin Brady.