Session-typed concurrent contracts (Q5925542)

The paper discusses the problem of checking that a subsystem of a concurrent system of a certain kind meets its specification. It is assumed that the subsystem and its user communicate via a bidirectional channel. A ``monitor'' process is put in between the subsystem and the user so that messages between the two go through the monitor, which can thus inspect them and raise an alarm if a message arrives at a wrong time or has wrong content. The monitor should not affect the behaviour of the system other than raising an alarm. A major part of the paper is devoted to how this can be checked. Another main topic is showing that whatever can be checked with subtypes, can be checked with monitors. The paper is more about verification using functional programming type theory than about concurrency. The concurrency model seems restrictive, and the paper says that deadlock freedom is not covered.