MobilityReadingGroup

Session-Ocaml: a Session-based Library with Polarities and Lenses

Keigo IMAI, Nobuko YOSHIDA, Shoji YUEN

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.

@article{IYY2019,
  author = {Keigo Imai and Nobuko Yoshida and Shoji Yuen},
  title = {{Session-Ocaml: a Session-based Library with Polarities and Lenses}},
  journal = {scico},
  pages = {1--50},
  publisher = {Elsevier},
  year = 2019
}

@article{IYY2019,
  author = {Keigo Imai and Nobuko Yoshida and Shoji Yuen},
  title = {{Session-Ocaml: a Session-based Library with Polarities and Lenses}},
  journal = {Science of Computer Programming},
  pages = {1--50},
  publisher = {Elsevier},
  doi = "10.1016/j.scico.2018.08.005",
  year = 2019
}