EdLambda - Type-driven Development with Idris, Edwin Brady

Who: Edwin Brady
Where: Skyscanner, 15 Lauriston Place
When: 7:30pm, Tuesday 9th May, 2017

Title: Type-driven Development with Idris


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.

to (Europe/London time)

More details: sites.google.com

More Information

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.

Quartermile One 15 Lauriston Place Edinburgh