Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2406.01456 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917683304333312 |
|---|---|
| author | Hirsch, Andrew K. |
| author_facet | Hirsch, Andrew K. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_01456 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Corps: A Core Calculus of Hierarchical Choreographic Programming Hirsch, Andrew K. Programming Languages 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. |
| title | Corps: A Core Calculus of Hierarchical Choreographic Programming |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2406.01456 |