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.
More details and tickets: www.eventbrite.co.uk
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.
