Speaker Sam Elliott. When 14 July, *at SkyScanner's offices at 15 Lauriston Place* 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
This is a ticketed event. To get a ticket: https://www.eventbrite.co.uk/e/erlang-meets-dependent-types-with-sam-elliott-tickets-17472346258 |