MobilityReadingGroup

π-calculus, Session Types research at Imperial College

セッション型のOCamlによるデザインと実装
Keigo IMAI , Shoji YUEN , Nobuko YOSHIDA
To appear in
Computer Software

Design and Implementation of Session Types in Ocaml

We propose session-ocaml, a novel library for session-typed concurrent/distributed programming in OCaml. Session-ocaml enables the session type inference only with the parametric polymorphism without employing the type-level programming framework as that of Haskell so that it can be applied to various statically-typed programming languages. The key ideas are following: (1) We give polarized session types as an alternative formulation of duality which enables OCaml to infer protocol in a session with a reasonable notational overhead. (2) We combine the parameterized monad with the data structure called ‘slots’ manipulated with the lenses technique, enabling full session type implementation including delegation of a session. We show a few application of session-ocaml including a simple SMTP client and a database server.

@article{IYY2017,
  author = {Keigo Imai and Shoji Yuen and Nobuko Yoshida},
  title = {{セッション型のOCamlによるデザインと実装}},
  journal = {Computer Software},
  pages = {1--25},
  publisher = {Iwanami Shoten},
  year = 2017
}
@article{IYY2017,
  author = {Keigo Imai and Shoji Yuen and Nobuko Yoshida},
  title = {{セッション型のOCamlによるデザインと実装}},
  journal = {Computer Software},
  pages = {1--25},
  publisher = {Iwanami Shoten},
  year = 2017
}