Coming Up‎ > ‎

October meetup: 08.10.2013

posted 3 Oct 2013, 08:53 by Ed Lambda   [ updated 15 Nov 2013, 07:05 ]
Who: Edwin Brady
When: Tuesday 8th October
Title: "State, interaction and side-effecting programs in Idris"

Idris ( 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.

Update: Edwin's slides are: here.