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. (c) 2022 Elsevier B.V. All rights reserved.
QueryAGT: Asynchronous global types in co-logic programming[Formula presented]
Bianchini R.;Dagnino F.
2023-01-01
Abstract
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. (c) 2022 Elsevier B.V. All rights reserved.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
