The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Un...
summary
A compositional interpreter builds a multi-token machine for Idealized Parallel Algol and implements terms as coloured Petri nets that run concurrent tokens over shared state and semaphores. The construction yields Petri strategies constrained by game-semantic types, and a proof shows computational adequacy with respect to the reference semantics. Petri strategies unfold to concurrent strategies on event structures, producing an operational causal description that matches the denotational causal account.
AI-written summary · about
chapters (11)
- 0:00Geometry of Causality intro
- 1:59Core methodology
- 3:37Computation model
- 9:29Web app interactions
- 11:26Original GOI limits
- 12:56Multi-token transition
- 14:18Multi-token machine
- 16:17Transformer contributions
- 17:53Interactive methodologies
- 20:45Model structure
- 24:49Closing remarks
related talks
20mCoarser Equivalences for Causal Concurrency
19mScenario-based Proofs for Concurrent Objects
01h 01mThe Future of Concurrency and Parallelism
30mCalculating Compilers for Concurrency
25mA Logical Interpretation of Asynchronous Multiparty Compatibility
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
27mC4: verified transactional objects
24mAn Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on(…)