Categorical Message Passing Language (CaMPL) for programmers

TL;DR

CaMPL is a novel functional-style concurrent programming language grounded in category theory, enabling safe message passing, controlled non-determinism, and flexible channel types with a formal type system ensuring deadlock-freedom.

Contribution

It introduces CaMPL, a new language combining category-theoretic semantics with advanced message passing features and a type system that guarantees deadlock-free concurrent programs.

Findings

CaMPL's type system prevents deadlocks and livelocks in programs.

Supports higher-order processes and custom channel datatypes.

Ensures formal correctness through a Curry-Howard-Lambek-like correspondence.

Abstract

Categorical Message Passing Language (CaMPL) is a functional-style concurrent programming language whose semantics is in category theory, more specifically, linear actegories. Its core programming feature is message passing along typed communication channels between concurrent processes. CaMPL also supports controlled non-determinism via 'races' which allow processes to adapt dynamically while they are running, higher-order processes which pass other processes as messages, and custom channel datatypes called protocols and coprotocols which allow one to define infinite channel types or implement session types. The type system of CaMPL arises from a Curry-Howard-Lambek-like correspondence for concurrent programming, established by Cockett and Pastro in their paper titled "The logic of message passing". This type system ensures that a formal CaMPL program, i.e., one which does not allow general recursion, will never become deadlocked or livelocked. In this article, we explore the type system of CaMPL, custom channel types, and controlled non-determinism using code examples after briefly introducing its mathematical underpinnings.