The Caml Hump: Opis

A functional-reactive approach for developing distributed systems in Objective Caml. In Opis, a protocol description consists of a reactive function (called event function) describing the behavior of a distributed system node. The event functions in Opis are built from pure functions as building blocks, composed using the Arrow combinators. This facilitates reasoning about event functions both informally and using interactive provers. For example, this approach leads to simple termination arguments.