Classical Processes in modern dress
summary
Proposes extending Curry–Howard to a Lambek-style correspondence that ties categorical models of classical linear logic to session-type semantics, and identifies the missing piece as a usable typed bisimulation or equational theory. Uses categorical tools (star-autonomous categories with a duality involution), instantiates models from sets and relations and domain-theoretic GoI to concurrent games/event structures, and reports CP’s practical problems (reductions on configurations not processes) with HCP’s hyperenvironments and mix partially fixing typing and simulation. Work in progress.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:04Classical processes modernized
- 2:51Rethink programming foundations
- 7:11Denotational semantics
- 10:20Simply typed Lambda basics
- 12:07Cartesian closed categories
- 15:21Modern tools in semantics
- 17:51Other languages and models
- 18:33Session types and linear logic
- 20:00History of concurrency
- 22:09Classical processes overview
- 23:34Semantics for session types
- 26:05Problems with CP calculus
- 27:31HCP improvements
- 28:34Family of models
- 30:23Future directions
- 30:44Summary
related talks
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem
19mMechanizing Session-Types using a Structural View: Enforcing Linearity without ...
01h 34mFormal Logic Undressed
15mCompiling with Continuations, Correctly
18mEpistemic Logic for Polyglots (Short Paper)
21mQuantum and Classical Control (work-in-progress)
11mLocal algebraic effect theories