Coming Up‎ > ‎

October Meetup - 02.10.2012

posted 26 Sep 2012, 09:02 by Ed Lambda
Who: Edwin Brady
When: Tuesday 2nd October, 7pm.
Title: Idris - a language with dependent types

Idris ( is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type, and verified by type checking.

Idris syntax is heavily influenced by Haskell, and features include type classes, records, and overloadable syntax. In this talk, I'll give a brief tour of dependently typed programming in Idris, by demonstration. In particular, I will show how Idris can be used to implement verifed domain specific languages.