Choreographic Programming in Modal Type Theory

on YouTube ↗21m

" summary

An instantiation of Modal Type Theory (MTT) maps Chorλ location annotations to modalities, adds two primitives—prepare (schedule a local value into a choreography) and broadcast (distribute projections to participants)—and shows how Core Lambda send/receive and a globalized list example are encoded; introduces two novel concepts common knowledge and local referencing to track distributed choice and local data, and conjectures that the translation can faithfully represent all of Chorλ.

AI-written summary · about

" chapters (10)

1. 0:00Introduction
2. 1:27Functional choreographic foundations
3. 2:28Local and global modalities
4. 3:56Type constructors in modal theory
5. 6:56Communication primitives
6. 9:46Reproducing Lambda communication
7. 12:17Globalizing local data
8. 14:06Extending modal theory
9. 16:36Conclusion
10. 16:56Q&A