Making Concurrency Functional
Glynn Winskel
Abstract
The article bridges between two major paradigms in computation, the functional, at basis computation from input to output, and the interactive, where computation reacts to its environment while underway. Central to any compositional theory of interaction is the dichotomy between a system and its environment. Concurrent games and strategies address the dichotomy in fine detail, very locally, in a distributed fashion, through distinctions between Player moves (events of the system) and Opponent moves (those of the environment). A functional approach has to handle the dichotomy more ingeniously, via its blunter distinction between input and output. This has led to a variety of functional approaches, specialised to particular interactive demands. Through concurrent games we can see what separates and connects the differing paradigms, and show how:
• to lift functions to strategies; how to turn functional dependency to causal dependency and so exploit functional techniques.
• several approaches of functional programming and logic arise naturally as full subcategories of concurrent games, including stable domain theory; nondeterministic dataflow; geometry of interaction; the dialectica interpretation; lenses and optics, and their extensions to containers in dependent lenses and optics.
• the enrichments of strategies (e.g. to probabilistic, quantum or real-number computation) specialise to the functional cases.
1 A core language for concurrent strategies derives from the mathematical structure, although we shall only glimpse it here in Section IV-G: it is higherorder and an interesting hybrid of dataflow, c f. T ensorFlow [ 4], concurrent process calculi, cf. CSP, CCS and Session Types
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext f0b290d8-2e65-47a0-8843-e33f37091549Cited by top-tier papers1
Ask how each one uses itRelated papers
- From Thin Concurrent Games to Generalized Species of StructuresPierre Clairambault, Federico Olimpieri, Hugo PaquetLICS 2023 · 3 citations
- The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal UnfoldingSimon Castellan, Pierre ClairambaultPOPL 2023 · 2 citations
- Proto-Quipper with Dynamic LiftingPeng Fu, Kohei Kishida, Neil J. Ross, Peter SelingerPOPL 2023 · 17 citations
- Concurrent Separation Logic Meets Template GamesPaul-André Melliès, Léo StefanescoLICS 2020 · 1 citation
- Modular Denotational Semantics for Effects with Guarded Interaction TreesDan Frumin, Amin Timany, Lars BirkedalPOPL 2024 · 13 citations
