Who: Edwin Brady
Where: Skyscanner, 15 Lauriston Place
When: 7:30pm, Tuesday 9th May, 2017
Title: Type-driven Development with Idris
Abstract
This talk will be about the book "Type-driven Development with Idris" (www.manning.com), recently published by Manning, and there will be an opportunity to win a copy.
Idris is a general purpose functional programming language with first-class dependent types, building on state-of-the-art techniques in programming language research. Idris aims to make type-based program verification techniques accessible to programming practitioners while supporting efficient systems programming via an optimising compiler and interaction with external libraries.
In this talk, I'll use a series of examples to show how Idris can be used for verifying realistic and important properties of software, from simple properties such as array bounds checking, to more complex properties of networked and concurrent systems.
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.
