Corps: A Core Calculus of Hierarchical Choreographic Programming

TL;DR

This paper addresses the challenge of giving a non-linear, agent-aware propositions-as-types interpretation for choreographic programming by leveraging doxastic logic. It introduces Corps, a core language for hierarchical choreographic programming that models data ownership with modalities like $\\square_A$ on a tree-structured topology and uses an authorization-logics-inspired channel via the $A \\mathrel{\\textsf{speaksfor}} B$ relation. The work outlines typing rules and topology-parameterized communication (CanDown, CanUp, CanSend), and articulates conjectures on endpoint projection, normalization, and noninterference, aiming to connect type-theoretic results with proof-theoretic results from authorization logic. If successful, this framework could yield deadlock-free, verifiable choreographies and unify concepts from functional choreographic languages (e.g., Pirouette, Chor\\lambda) with authorization/doxastic logics, enriching both fields and offering new avenues for concurrency theory.

Abstract

Functional choreographic programming suggests a new propositions-as-types paradigm might be possible. In this new paradigm, communication is not modeled linearly; instead, ownership of a piece of data is modeled as a modality, and communication changes that modality. However, we must find an appropriate modal logic for the other side of the propositions-as-types correspondence. This paper argues for doxastic logics, or logics of belief. In particular, authorization logics -- doxastic logics with explicit communication -- appear to represent hierarchical choreographic programming. This paper introduces hierarchical choreographic programming and presents Corps, a language for hierarchical choreographic programming with a propositions-as-types interpretation in authorization logic.

Figures (3)

• Figure 1: Syntax of Doxastic Logic
• Figure 2: Selected Rules for Doxastic Logic and Authorization Logic
• Figure 3: Corp Selected Syntax and Typing Rules