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 and delegations. We show applications of session-ocaml including a travel agency usecase and an SMTP protocol.

@inproceedings{IYY2017,
  author = {Keigo Imai and Nobuko Yoshida and Shoji Yuen},
  title = {{Session-ocaml: a session-based library with polarities and lenses
}},
  booktitle = {19th International Conference on Coordination Models and Languages},
  series = {LNCS},
  volume = {10319},
  pages = {99--118},
  publisher = {Springer},
  year = 2017
}

@inproceedings{IYY2017,
  author = {Keigo Imai and Nobuko Yoshida and Shoji Yuen},
  title = {{Session-ocaml: a session-based library with polarities and lenses
}},
  booktitle = {19th International Conference on Coordination Models and Languages},
  series = {LNCS},
  volume = {10319},
  pages = {99--118},
  publisher = {Springer},
  doi = "10.1007/978-3-319-59746-1_6",
  year = 2017
}