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.

翻译：函数式编排编程暗示了一种新的命题即类型范式可能成立。在这一新范式中，通信并非以线性方式建模；相反，数据片段的拥有权被建模为一种模态，而通信则改变该模态。然而，我们必须为命题即类型对应的另一侧寻找一种合适的模态逻辑。本文主张采用信念逻辑（doxastic logics），即关于信念的逻辑。具体而言，授权逻辑——一种具有显式通信的信念逻辑——似乎能够表示层次化编排编程。本文介绍了层次化编排编程，并提出了Corps，这是一种用于层次化编排编程的语言，其在授权逻辑中具有命题即类型的解释。