An OCaml Implementation of Binary Sessions

HERNÁN MELGRATTI; LUCA PADOVANI

Behavioural Types: from Theory to Tools

River Publishers

Año: 2017;

In this chapter we describe FuSe, a simple OCaml module that implements binary sessions and enables a hybrid form of session type checking without resorting to external tools or extensions of the programming language. The approach combines static and dynamic checks: the former ones are performed at compile time and concern the structure of communication protocols; the latter ones are performed as the program executes and concern the linear usage of session endpoints. We recall the minimum amount of theoretical background for understanding the essential aspects of the approach (Sec- tion 11.1) and then describe the API of the OCaml module throughout a series of simple examples (Section 11.2). In the second half of the chapter we detail the implementation of the module (Section 11.3) and discuss a more complex and comprehensive example, also arguing about the effectiveness of the hybrid approach with respect to the early detection of protocol vio- lations (Section 11.4). We conclude with a survey of closely related work (Section 11.5).