Selected papers from the 15th international symposium on Theoretical Aspects of Software Engineering (TASE 2021)

Global types are at the core of communication-based programming. They allow a high-level specification of protocols involving many participants and enforce good safety and liveness properties, such as deadlock freedom, and the absence of locked participants and orphan messages. The present software provides an implementation in co-logic programming of a novel formalism of global types for sessions with asynchronous communications, where we use coinduction to properly handle the coinductive syntax of global types and processes. It also offers a simple query language to write sessions and global types, providing primitives for type checking.