Personal tools
You are here: Home Events LFCS seminar: Edwin Brady: State machines all the way down

LFCS seminar: Edwin Brady: State machines all the way down

— filed under: ,

  • LFCS Seminar
  • Upcoming events
When Apr 12, 2017
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal

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

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.


Document Actions