You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Pastel Raschke (May 10 2020 at 08:25):@Henry Story i think you might want to check out these papers
a linear/producer/consumer model for classical linear logic (technical report)
lpc generalizes the linear-nonlinear adjoint presentation of multiplicative intuitionistic (and classical) linear logic by splitting the persistent mode into an intuitionistic producer (for !) and a cointuitionistic consumer (for ?), which allows them to be interpreted by more dual pairs of categories than a category and its own dual
linear logic for constructive mathematics
classical linear (actually affine) logic has an involutive de morgan duality which trades the roles of proof and refutation. in intuitionism many concepts are bifurcated into two de morgan duals, like equality and apartness.
a chu construction (Chu(H,0) where H is a heyting algebra) lets you interpret intuitionistic connectives into additives that bundle these dual definitions together (constructive proof and refutation), and classical connectives into multiplicatives that admit constructive proofs by contradiction (you can only use an assumption once, instead of several times with different values and not specifying which one is the witness)
nelson logic is modeled by Chu(H, 1), and instead of being affine and requiring the underlying half-propositions p+ and p- = 0, it is mix
Henry Story (May 10 2020 at 08:32):Thanks for the pointers to help me get out of the very interesting rabbit hole I am in :-)
That should help me slowly get back from making sure my basics of (co)Topoi are solid, to Abramski's Game Semantics for Linear Logic, and from there to session types to analyze protocols on the web.
(I guess the linearity comes in simply because games require the players to take turns, which is a linear phenomenon, and that is what knits the topoi and complement topoi together.)
I just found this very interesting talk relating Game Semantics and Session Types, as two ways to analyse protocols https://dl.acm.org/doi/abs/10.1145/3290340 https://www.youtube.com/watch?v=px38U3jsOLQ
- The 🐟 BabelFish (@bblfish) Pastel Raschke (May 10 2020 at 09:22):mellies and mimram have done work on asynchronous games (innocence without alternation) which i have not yet read, and mellies has also done work on template games which is related to scheduling and synchronization
i'm not sure how that gels with synchronous pi-calculus being more expressive than asynchronous pi-calculus. also, wen kokke has been working on hypersequent classical processes which reconciles the proof-process correspondence between classical linear logic and session-typed pi-calculus with delayed actions (non-blocking i/o)
Pastel Raschke (May 10 2020 at 09:35):ah, that paper cites asynchronous games. also note concurrency is related to directed spaces and directed homotopy, which hopefully will result in some sort of directed homotopy type theory as an internal language of omega-topoi, whatever those are (currently higher topoi are mere (∞,1)-topoi)