EdLambda: Erlang meets Dependent Types, 14th July at Skyscanner's offices

[Rob Stewart]

Hi folks,

EdLambda is back on in July. This time will be slightly different,
we're being very kindly hosted by Skyscanner, an arrangement
instigated by Mike Moran. Sponsorship is: a room with projection
facilities, pizza and beer. (Thanks Mike and Skyscanner!)

Skyscanner have asked that we have a list of people entering their
offices, so we've an EventBrite page to obtain a list of people
attending. Register here:

https://www.eventbrite.co.uk/e/erlang-meets-dependent-types-with-sam-elliott-tickets-17472346258

Who: Sam Elliott
When: 14 July at 18:00
Where: Skyscanner - 15 Lauriston Place Edinburgh

Title: Erlang meets Dependent Types

Concurrent programming is notoriously difficult, due to needing to reason
not only about the sequential progress of any algorithms, but also about
how information moves between concurrent agents. What if programmers were
able to reason about their concurrent programs and statically verify both
sequential and concurrent guarantees about those programs’ behaviour? That
would likely reduce the number of bugs and defects in concurrent systems.

Erlang’s existing type system cannot produce particularly strong
guarantees, especially not with regards to concurrent systems. In this talk
I will describe work to integrate a dependently-typed language (Idris) with
Erlang, in order to integrate dependently-typed code with Erlang programs.
This work included both a new Idris code generator, and libraries for
reasoning about concurrent Erlang programs, including some OTP behaviours.

[Rob Stewart]

Hi folks,

A reminder that if you'd like to come to EdLambda this Tuesday, hosted
by SkyScanner at their offices (with free pizza and beer), then you'll
need to register on EventBrite.

https://www.eventbrite.co.uk/e/erlang-meets-dependent-types-with-sam-elliott-tickets-17472346258