EdLambda: Erlang meets Dependent Types

Speaker Sam Elliott.

Abstract

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.

to (Europe/London time)

More details and tickets: www.eventbrite.co.uk

More Information

Attending: koshatnik

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
EH3 9EN