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

Science of Computer Programming(2019)

引用 33|浏览58
暂无评分
摘要
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.
更多
查看译文
关键词
Session types,Functional programming,Parametric polymorphism,Lenses,OCaml
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要