Typechecking Protocols with Mungo and StMungo: A Session Type Toolchain for Java

Dimitrios Kouzapas, Ornela Dardha, Roly Perera, Simon J. Gay

Research output: Contribution to journalArticlepeer-review

Abstract

Static typechecking is an important feature of many standard programming languages. However, static typing focuses on data rather than communication, and therefore does not help programmers correctly implement communication protocols in distributed systems. The theory of session types provides a basis for tackling this problem; we use it to develop two tools that support static typechecking of communication protocols in Java. The first tool, Mungo, extends Java with typestate definitions, which allow classes to be associated with state machines defining permitted sequences of method calls: for example, communication methods. The second tool, StMungo, takes a session type describing a communication protocol, and generates a typestate specification of the permitted sequences of messages in the protocol. Protocol implementations can be validated by Mungo against their typestate definitions and then compiled with a standard Java compiler. The result is a toolchain for static typechecking of communication protocols in Java. We formalise and prove soundness of the typestate inference system used by Mungo, and show that our toolchain can be used to typecheck a client for the standard Simple Mail Transfer Protocol (SMTP).
Original languageEnglish
Pages (from-to)52-75
Number of pages46
JournalScience of Computer Programming
Volume155
Early online date5 Dec 2017
DOIs
Publication statusPublished - 1 Apr 2018

Fingerprint

Dive into the research topics of 'Typechecking Protocols with Mungo and StMungo: A Session Type Toolchain for Java'. Together they form a unique fingerprint.

Cite this