Idris (idris-lang.org) is a general-purpose purely functional
programming language with dependent types. In a talk at EdLambda last
year, I gave an introduction to the language showing how to implement
small functions, prove their correctness, and gave a larger example of
a well-typed interpreter for the lambda calculus.
In this talk, I will present some recent work on Idris which gives a
more practical example of these techniques. I will show how we can use
dependent types to implement and reason about side-effecting programs,
with a clear and usable API, illustrated using a "Space Invaders"
style game.
The Outhouse
12A Broughton Street Lane
Edinburgh
EH1 3LY
More details: sites.google.com
About EdLambda
EdLambda is an Edinburgh group for people interested in functional programming which has been running since September 2010. We meet in the Outhouse pub on the 2nd Tuesday of every month at 7pm. There is usually a talk on a subject of interest to functional programmers, followed by chat and drink! EdLambda meetups are free events and everyone is welcome.
