David Janin

Researcher at LaBRI, Bordeaux University

Researcher at LaBRI, Bordeaux University, with a strong background in Logic and Automata theory, I’m now interested in designing programing language features that can be used for arts (music, drawing, animation) by artists themselves. For such a purpose, I am considering various extension of typed functional languages via new algebraic data (e.g. overlapping tiles) or extended monads (e.g. timed monads).

An equational modeling of asynchronous concurrent programming

Asynchronous concurrent programing is a widely spread technique offering some simple concurrent primitives that are restricted in such a way that the resulting concurrent programs are dead-lock free.

In this paper, we develop and study a formal model of the underlying application programmer interface. For such a purpose, we formally define the extension of a monad by some notion of monad references uniquely bound to running monad actions together with the associated asynchronous primitives fork and read. The expected semantics is specified via two series of equations relating the behavior of these extension primitives with the underlying monad primitives.

This allows for formally stating and proving various properties of the resulting model of asynchronous programing. As a particular case, we eventually recover the notion of promises and we formally prove that, under simple further restrictions, promises induce a monad isomorphic to the underlying monad. This also allows for lifting asynchronous concurrent programming to data-flow concurrent programing.

Our proposal is illustrated throughout by concrete extensions of Haskell IO monad that allows for assessing the validity of the proposed equations and for showing how closely our proposal is related with existing libraries.

Video ←Back