Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Thu 7 Sep 2017 09:05 - 10:00 at L3 - Invited talk Chair(s): Sam Lindley

A useful pattern in dependently typed programming is to define a state transition system, for example the states and operations in a network protocol, as an indexed monad. We index each operation by its input and output states, thus guaranteeing that operations satisfy pre- and post-conditions, by typechecking. However, what if we want to write a program using several systems at once? What if we want to define a high level state transition system, such as a network application protocol, in terms of lower level states, such as network sockets and mutable variables?

In this talk, I will present an architecture for dependently typed applications based on a hierarchy of state transition systems, implemented in a generic data type ST. This is based on a monad indexed by contexts of resources, allowing us to reason about multiple state transition systems in the type of a function. Using ST, we show: how to implement a state transition system as a dependent type, with type level guarantees on its operations; how to account for operations which could fail; how to combine state transition systems into a larger system; and, how to implement larger systems as a hierarchy of state transition systems. I will illustrate the system with a high level network application protocol, implemented in terms of POSIX network sockets.

Lecturer in Computer Science at the University of St Andrews

Thu 7 Sep

09:05 - 10:00: ML 2017 - Invited talk at L3
Chair(s): Sam LindleyUniversity of Edinburgh, UK
mlfamilyworkshop-2017-papers150476790000009:05 - 10:00
Edwin BradyUniversity of St. Andrews, UK