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. |
Coming Up >