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). The source code of FuSe, which is partially described in this chapter and can be used to compile and run all the examples given therein, can be downloaded from the second author’s home page.

Melgratti, H., Padovani, L. (2017). An OCaml Implementation of Binary Sessions. NLD : River Publishers.

An OCaml Implementation of Binary Sessions

PADOVANI, Luca
2017

Abstract

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). The source code of FuSe, which is partially described in this chapter and can be used to compile and run all the examples given therein, can be downloaded from the second author’s home page.
2017
Behavioural Types: from Theory to Tools
243
263
Melgratti, H., Padovani, L. (2017). An OCaml Implementation of Binary Sessions. NLD : River Publishers.
Melgratti, Hernán; Padovani, Luca
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/997786
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 0
social impact