Corps: A Core Calculus of Hierarchical Choreographic Programming

TL;DR

This paper introduces Corps, a language for hierarchical choreographic programming based on a propositions-as-types approach using authorization logic, enabling structured communication and ownership modeling in distributed systems.

Contribution

It proposes a novel paradigm of functional choreographic programming with a propositions-as-types interpretation in authorization logic, and introduces the Corps language for hierarchical choreographies.

Findings

Corps enables structured hierarchical choreographies.

The approach models ownership and communication via modalities.

It demonstrates the viability of doxastic logics for choreographic programming.

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.