Who: Edwin Brady

When: Tuesday 8th October

Title: "State, interaction and side-effecting programs in Idris"

Abstract:

Idris (http://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.

Update: Edwin's slides are: here.