2024/06/03 by Andrew K. Hirsch, Hirsch, Andrew K. · 1 citation
Computer Science · Engineering · #Artificial Intelligence in Games #FOS: Computer and information sciences #Human Motion and Animation #Programming Languages (cs.PL) #Robotic Path Planning Algorithms
paper · pdf · doi:10.48550/arxiv.2406.01456
openalex publication_date 2024/06/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.