Treffer: Session-ocaml: A session-based library with polarities and lenses.

Abstract We propose session-ocaml, a novel library for session-typed concurrent/distributed programming in OCaml. Our technique solely relies on parametric polymorphism, which can encode core session type structures with strong static guarantees. Our key ideas are: (1) polarised session types , which give an alternative formulation of duality enabling OCaml to automatically infer an appropriate session type in a session with a reasonable notational overhead; and (2) a parameterised monad with a data structure called ' slots ' manipulated with lenses , which can statically enforce session linearity including delegations. We introduce a notational extension to enhance the session linearity for integrating the session types into the functional programming style. We show applications of session-ocaml to a travel agency use case and an SMTP protocol implementation. Furthermore, we evaluate the performance of Image 1 on a number of benchmarks. Highlights • The first library of session types in OCaml with static type checking. • No modification required in the OCaml compiler. • The polarised session types for simple duality inference. • A new encoding based on parameterised monad with reasonable performance. • Linear pattern matching for the monad, enabling labelled branching of sessions. [ABSTRACT FROM AUTHOR]