EdLambda - Type-driven Development with Idris, Edwin Brady
Description changed:
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" (https://www.manning.com/books/type-driven-development-with-idris), 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.
