Corps: A Core Calculus of Hierarchical Choreographic Programming
summary
Claims that choreographic located types correspond to doxastic modalities and that adding explicit trust yields authorization logic as the right propositions-as-types for hierarchical choreographies. Presents a new core language called Core (Corps) that encodes tree‑like agent hierarchies via modal contexts and a "lock" type constructor derived from flow‑limited authorization work. Reports implementations of the syntax and type system with progress and preservation proofs, ongoing proofs of canonicalization and projection correctness, and notes communication forces rethinking beta equivalence (options: separate comm reductions, trace equality, or treat communication as pure modality change).
AI-written summary · about
chapters (20)
- 0:00Corps intro
- 1:59Types in choreographies
- 3:05PureET vs Lambda calculus
- 6:58PureET limitations
- 8:25Hierarchical choreographies
- 9:50Representing hierarchies
- 11:56Authorization in choreographies
- 13:48Logic calculi
- 15:55Beta equivalence challenges
- 17:23Future work
- 18:04Conclusion & Q&A
- 19:08Masquerade intro
- 20:11Info flow security
- 23:02Type system for labels
- 25:51Multi-threading challenges
- 27:37Masquerade overview
- 29:00Declassification policies
- 30:45Formal model
- 31:26Non-interference proof
- 31:48Q&A on side channels
related talks
32mSubstructural Information Flow via Polymorphism
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
23mSecurity Reasoning via Substructural Dependency Tracking
58mAutomating Relational Verification of Infinite-State Programs
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
36mObject Capabilities
18mCertifying Derivation of State Machines from Coroutines
25mCapabilities, Effects, Ownership, and Behaviors