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.
Mike Stay (Apr 21 2020 at 17:51):Back in around 2012, Jamie Vicary pointed out to me that the string diagrams for adjointness, in the case where one of the objects is the monoidal unit, are very suggestive of synchronization in the pi calculus:
synch.png
Mike Stay (Apr 21 2020 at 17:53):I found that I could interpret nearly all of the syntax of pi calculus in a compact closed bicategory and that reductions were exclusively due to adjointness. Here's the internal monoid object for parallel composition of processes:
Mike Stay (Apr 21 2020 at 17:54):
Mike Stay (Apr 21 2020 at 17:55):Names are morphisms in or out of the monoidal unit with adjoints:
Mike Stay (Apr 21 2020 at 17:57):
Mike Stay (Apr 21 2020 at 18:00):Parallel composition has an adjoint:
par.png
Mike Stay (Apr 21 2020 at 18:09):The communication reduction looks like this. We're sending a name z on a name x (green). We're listening on a name x for a name we'll call y (purple); when we get one, we'll do Q. The result of the two processes interacting is Q with z replacing y. Note that y is a bound variable, so its name doesn't appear anywhere in the diagram.
Mike Stay (Apr 21 2020 at 18:09):
Mike Stay (Apr 21 2020 at 18:11):The problem is that there are more reductions in the compact closed bicategory than in the pi calculus. For example, if another copy of x? occurred in Q, x! could synchronize with that one instead, which is not allowed in pi calculus.
Mike Stay (Apr 21 2020 at 18:16):One way of dealing with this problem is by compiling the pi calculus terms down to Yoshida's combinators, where there are no "closures". Instead, as execution progresses, links between distinct names are created.
Mike Stay (Apr 21 2020 at 18:19):I've got string diagrams for each of the combinators. The remaining issue is how to introduce fresh names. Recent work on second order algebraic theories look promising. It would take some work to adapt it to the compact-closed-bicategory case instead of the cartesian-category-with-exponentiable-object case.
Mike Stay (Apr 21 2020 at 18:23):If anyone's interested in exploring this, let me know and we can start a stream.
Nathanael Arkor (Apr 21 2020 at 18:35):Mike Stay said:
I've got string diagrams for each of the combinators. The remaining issue is how to introduce fresh names. Recent work on second order algebraic theories look promising. It would take some work to adapt it to the compact-closed-bicategory case instead of the cartesian-category-with-exponentiable-object case.
Maybe I can rephrase to see if I understand? It looks like compact-closed bicategories play a similar role (though perhaps not completely analogous) for the π-calculus as do CCCs for the STLC? If this is the case, then we wouldn't expect to use compact-closed bicategories instead of second-order algebraic theories: each SOAT would induce a compact-closed bicategory. For the STLC, for instance, we have an equivalence between models for the SOAT for the STLC and CCCs.
Nathanael Arkor (Apr 21 2020 at 18:35):I'm not familiar; is there a standard internal language correspondence for the π-calculus already?
Nathanael Arkor (Apr 21 2020 at 18:35):In any case, this seems very interesting.
Christian Williams (Apr 21 2020 at 18:46):so what should we make, #concurrency ?
Nathanael Arkor (Apr 21 2020 at 18:54):It could go in the #theory: type theory stream for the time being?
Chad Nester (Apr 21 2020 at 19:32):I'd read a concurrency stream, although I think it should be separate from type theory
Chad Nester (Apr 21 2020 at 19:35):@Mike Stay I think that looks interesting. It reminds me of "interaction nets" , which, iirc, also admit interpretation in a compact closed bicategory.
Chad Nester (Apr 21 2020 at 19:39):@Nathanael Arkor nope! There's no satisfactory, Curry-Howard-Lambek sort of thing for the pi-calculus
Mike Stay (Apr 21 2020 at 19:50):Christian Williams said:
so what should we make, #concurrency ?
Sounds good to me.
Mike Stay (Apr 21 2020 at 19:59):Chad Nester said:
Mike Stay I think that looks interesting. It reminds me of "interaction nets" , which, iirc, also admit interpretation in a compact closed bicategory.
Thanks! The immediate difference I see is that interaction nets are strongly confluent, while pi calculus is certainly not.
Valeria de Paiva (Apr 21 2020 at 20:52):Mike Stay said:
Chad Nester said:
Mike Stay I think that looks interesting. It reminds me of "interaction nets" , which, iirc, also admit interpretation in a compact closed bicategory.
Thanks! The immediate difference I see is that interaction nets are strongly confluent, while pi calculus is certainly not.
well, there is Bellin's very old work https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.3948 and not so old work
On the π-calculus and distributed calculi for co-intuitionistic logic too!
sarahzrf (Apr 21 2020 at 21:46):o_o
sarahzrf (Apr 21 2020 at 21:47):is a compact closed bicategory one where every 1-cell has a left & right adjoint, or what?
sarahzrf (Apr 21 2020 at 21:48):oh, it's more directly analogous?
sarahzrf (Apr 21 2020 at 22:02):@Mike Stay i dont follow what the diagrams have to do with adjointness or the pi calculus? :sweat_smile: would you be willing to explain starting a little earlier what the correspondence is between pi-calculus objects and categorical objects?
sarahzrf (Apr 21 2020 at 22:03):& where is a monoid object coming in?
Mike Stay (Apr 21 2020 at 22:11):The pi calculus is a toy programming language invented by Robin Milner in the 90s, a successor to CCS. The grammar pi calculus involves both names (which I denote by an object N) and processes (P). P forms a commutative monoid with multiplication | and identity 0. Processes can also be formed by sending (!:N ⊗ N -> P), receiving (?:N ⊗ (N -> P) -> P) and generating a fresh name (ν: (N -> P) -> P).
Mike Stay (Apr 21 2020 at 22:11):The one reduction rule is the "comm" rule:
comm: x!(z) | x?(y).Q => Q { z / y }
sarahzrf (Apr 21 2020 at 22:11):oh i know the pi calculus
Mike Stay (Apr 21 2020 at 22:11):Note that the pi calculus is not confluent:
x!(z1) | x!(z2) | x?(y).Q
may reduce either to
x!(z2) | Q { z1 / y } or x!(z1) | Q { z2 / y }.
Mike Stay (Apr 21 2020 at 22:11):OK, so what's your question?
sarahzrf (Apr 21 2020 at 22:12):well, how are you corresponding pi-calculus objects to categorical objects? each term becomes a 1-cell, or what?
sarahzrf (Apr 21 2020 at 22:12):and if so, what is the type of the 1-cell given by a term?
Mike Stay (Apr 21 2020 at 22:12):Each term is a 1-cell of type P.
sarahzrf (Apr 21 2020 at 22:13):"of type P"?
sarahzrf (Apr 21 2020 at 22:13):you mean from the monoidal unit to P, or what?
Mike Stay (Apr 21 2020 at 22:13):Closed terms (those with no free variables/names) are morphisms from the monoidal unit to P, yes.
sarahzrf (Apr 21 2020 at 22:13):kk
sarahzrf (Apr 21 2020 at 22:14):oh, so more generally, do you do like.... N ⊗ N ⊗ N → P for sth with 3 free variables/names?
Mike Stay (Apr 21 2020 at 22:14):Yes.
sarahzrf (Apr 21 2020 at 22:15):ohhh, ok, & then the adjointness stuff plays in because you can't directly compose, reflecting how you don't directly substitute?
sarahzrf (Apr 21 2020 at 22:15):does N have to be self-dual or something?
Mike Stay (Apr 21 2020 at 22:16):In a compact closed bicategory, all objects have duals.
sarahzrf (Apr 21 2020 at 22:16):yeah, but an object's dual might not be canonically isomorphic to it
Mike Stay (Apr 21 2020 at 22:17):But there are cap and cup that let us draw string diagrams.
sarahzrf (Apr 21 2020 at 22:17):yeah, i have familiarity with compact closed 1-categories
Mike Stay (Apr 21 2020 at 22:17):Prof is a compact closed bicategory.
Mike Stay (Apr 21 2020 at 22:18):Cocont (categories, cocontinuous functors, nat'l transformations) is equivalent, but composition is strict, so easier to think about.
sarahzrf (Apr 21 2020 at 22:18):i have your paper pulled up in another window :)
sarahzrf (Apr 21 2020 at 22:18):the pages and pages of coherence conditions are terrifying :scream:
Mike Stay (Apr 21 2020 at 22:19):Ah, but there are patterns in the coherence laws!
sarahzrf (Apr 21 2020 at 22:19):i was hoping so :>
sarahzrf (Apr 21 2020 at 22:19):someday i will get around to learning them...
sarahzrf (Apr 21 2020 at 22:20):but in any case—so, hmm, this treatment sort of suggests a distinction between names and variables-for-names, doesnt it?
Mike Stay (Apr 21 2020 at 22:21):E.g. the associahedra have a Catalan number of vertices and lower associahedra as "faces". The unitors go between two associahedra, the second with one fewer object.
sarahzrf (Apr 21 2020 at 22:21):catalan numbers!
Nathanael Arkor (Apr 21 2020 at 22:22):Is there an established internal language for compact closed categories? E.g. as some kind of multiplicative fragment of classical linear logic?
sarahzrf (Apr 21 2020 at 22:22):abstract index notation :>
Nathanael Arkor (Apr 21 2020 at 22:23):It would be interesting to derive a relationship between the π-calculus and linear logic, if both can be used as internal languages of compact closed bicategories.
sarahzrf (Apr 21 2020 at 22:23):half serious
Mike Stay (Apr 21 2020 at 22:23):distinction between names and variables
Milner himself in later treatments refactored "new" and "input" into "fresh" and lambda. In that way of looking at it, names are what variables hold.
sarahzrf (Apr 21 2020 at 22:23):yeah thats basically what i figured
sarahzrf (Apr 21 2020 at 22:23):sounds like good hygeine
sarahzrf (Apr 21 2020 at 22:23):like assignables vs variables
sarahzrf (Apr 21 2020 at 22:24):hmmmmm...... but: is it just me, or is there an awful lot of cartesianness to the pi calculus which is not available in this setup?
sarahzrf (Apr 21 2020 at 22:24):names would have to be a comonoid wouldnt they?
Mike Stay (Apr 21 2020 at 22:25):@Nathanael Arkor Wadler came up with a calculus for linear logic that looks like a certain synchronous pi calculus.
sarahzrf (Apr 21 2020 at 22:26):is that one of the later dual calculi
Mike Stay (Apr 21 2020 at 22:27):names would have to be a comonoid
Yes, because pi calculus allows you to duplicate names, names have to be a comonoid. I haven't worked through all the details of that.
Nathanael Arkor (Apr 21 2020 at 22:27):Mike Stay said:
Nathanael Arkor Wadler came up with a calculus for linear logic that looks like a certain synchronous pi calculus.
Very interesting: Propositions as Sessions (https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-sessions/propositions-as-sessions.pdf).
sarahzrf (Apr 21 2020 at 22:28):god i should catch up on wadler's linear stuff
sarahzrf (Apr 21 2020 at 22:28):ive read like 1 and a half papers of it...
Mike Stay (Apr 21 2020 at 22:28):Abramsky, of course, wrote "Computational Interpretations of Linear Logic", in which he gives "process calculi", but it's not pi calculus by any means.
sarahzrf (Apr 21 2020 at 22:28):oh i know that one super well :sunglasses:
sarahzrf (Apr 21 2020 at 22:29):it's the basis of one of the projects im doing for my degree
sarahzrf (Apr 21 2020 at 22:29):it's in my backpack right now lol
sarahzrf (Apr 21 2020 at 22:31):ooh yeah i actually remember thinking before about the fact that the communication rule in PE₂ corresponds to reducing a cut connected to an axiom link in a proof net & it looks suspiciously like a yanking
sarahzrf (Apr 21 2020 at 22:31):& then i went and thought "it's 'communication'... and it's a yanking... hahahahaha it's quantum teleportation"
sarahzrf (Apr 21 2020 at 22:32):i completely forgot abt that
sarahzrf (Apr 22 2020 at 02:00):@Mike Stay ok, im looking again at the diagrams and i'm still finding them confusing :\
sarahzrf (Apr 22 2020 at 02:00):in the first one: what does the labelling on the wires mean? should they say "N" instead of "x"?
sarahzrf (Apr 22 2020 at 02:01):but "x" isn't a pi calculus process anyway, is it?
sarahzrf (Apr 22 2020 at 02:01):or in the 3rd one: where is N ≅ N* ⊗ P coming from?
sarahzrf (Apr 22 2020 at 02:03):hm, are the diagrams depicting some kind of async calculus w/ different types from the ones you wrote as in
Processes can also be formed by sending (!:N ⊗ N -> P), receiving (?:N ⊗ (N -> P) -> P) and generating a fresh name (ν: (N -> P) -> P).
John Baez (Apr 22 2020 at 02:46):sarahzrf said:
is a compact closed bicategory one where every 1-cell has a left & right adjoint, or what?
This was already answered by now but anyway:
"Compact closed" hints at symmetric monoidal - for example a merely monoidal category where every object has a left & right adjoint is not called compact closed, it's called rigid. So what you're talking about deserves to be called a rigid bicategory (though I've never heard anyone say that).
A compact closed bicategory is a symmetric monoidal bicategory where every 1-cell has a left pseudoadjoint, or equivalently a right pseudoadjoint.
John Baez (Apr 22 2020 at 02:47):@Mike Stay wrote about these in his thesis:
Abstract. A compact closed bicategory is a symmetric monoidal bicategory where every object is equipped with a weak dual. The unit and counit satisfy the usual "zig-zag" identities of a compact closed category only up to natural isomorphism, and the isomorphism is subject to a coherence law. We give several examples of compact closed bicategories, then review previous work. In particular, Day and Street defined compact closed bicategories indirectly via Gray monoids and then appealed to a coherence theorem to extend the concept to bicategories; we restate the definition directly.
We prove that given a 2-category T with finite products and weak pullbacks, the bicategory of objects of C, spans, and isomorphism classes of maps of spans is compact closed. As corollaries, the bicategory of spans of sets and certain bicategories of "resistor networks" are compact closed.
Chad Nester (Apr 22 2020 at 05:40):Regarding Wadler's "propositions ad sessions", while he uses pi-calculus like names for the terms of his type theory, I don't think it has all that much to do with the pi calculus.
Chad Nester (Apr 22 2020 at 05:42):Also there's a slightly earlier paper called "the logic of message passing" by Cockett and Pastro that gives a more powerful / general system, capturing Wadler's work as a degenerate case (including the interpretation of the multiplicatives). Unfortunately it's a pretty daunting paper to read.
Chad Nester (Apr 22 2020 at 05:42):Very much in the line of work started by Bellin and Scott though!
Christian Williams (Apr 22 2020 at 06:20):@Mike Stay could you change the topic of your first message in this thread? to break it off from general "pictures".
We can start the concurrency stream tomorrow.
Robin Piedeleu (Apr 22 2020 at 08:06):Chad Nester said:
Mike Stay I think that looks interesting. It reminds me of "interaction nets" , which, iirc, also admit interpretation in a compact closed bicategory.
Do you have a reference for this? I've been working on interaction nets recently and, while a bicategorical interpretation also seemed to make sense to me, I did not find any paper on the topic.
Robin Piedeleu (Apr 22 2020 at 08:28):Mike Stay said:
The problem is that there are more reductions in the compact closed bicategory than in the pi calculus. For example, if another copy of x? occurred in Q, x! could synchronize with that one instead, which is not allowed in pi calculus.
Could you introduce an additional edge coming out of the 'send' and 'receive' generators to represent communication explicitly? The new reduction rule for these ternary nodes would then be dual to the one you have given for parallel composition. This eliminates some of the nondeterminism (but the commutativity of parallel composition preserves some degree of non-confluence).
Chad Nester (Apr 22 2020 at 09:18):I was thinking about section 3.4 of
lafont-1997-interaction-combinators.pdf
Chad Nester (Apr 22 2020 at 09:18):(@Robin Piedeleu )
Chad Nester (Apr 22 2020 at 09:19):while not explicitly categorical, the notation is the same
Chad Nester (Apr 22 2020 at 09:24):There are probably some fun things to work out with concerning how interaction nets relate to linear combinatory algebras via the geometry of interaction, now that I think about it.
Mike Stay (Apr 22 2020 at 16:31):sarahzrf said:
in the first one: what does the labelling on the wires mean? should they say "N" instead of "x"?
In the first one X is any arbitrary type. It's what Jamie showed me.
sarahzrf (Apr 22 2020 at 16:37):ooooooooooooh wait i see how it's a yanking now ._.
sarahzrf (Apr 22 2020 at 16:38):but can't that only work if the other object is also the monoidal unit?
sarahzrf (Apr 22 2020 at 16:38):duals are unique, aren't they? and the monoidal unit is self-dual?
Mike Stay (Apr 22 2020 at 16:45):sarahzrf said:
or in the 3rd one: where is N ≅ N* ⊗ P coming from?
None of this is set in stone. Given a name, you can send and receive on it, so I was trying to capture that here. A different option I considered was having ! and ? morphisms, each of which took N as an input, and were only adjoint when the names matched:
alternate.png
This one treats names more like variables and various other things get easier, but the adjunction is a little harder to see.
sarahzrf (Apr 22 2020 at 16:47):but where is N ≅ N* ⊗ P coming from?
sarahzrf (Apr 22 2020 at 16:48):i don't follow at all
sarahzrf (Apr 22 2020 at 16:48):it's not that i think there's something wrong with it, i just don't get what that might mean as an option
sarahzrf (Apr 22 2020 at 16:49):like, what does the map N* ⊗ P → N do?
Mike Stay (Apr 22 2020 at 16:52):Going the other way, given a morphism 1->N, you get a morphism 1->N* ⊗ P with an adjoint that you can use to send some other name on. So given (z) you get (z!)
sarahzrf (Apr 22 2020 at 16:58):the talk is about to start, i'll ask more later :T
sarahzrf (Apr 22 2020 at 16:58):i think i might need to look at a specific model, i may be thinking too syntactically about this
Mike Stay (Apr 22 2020 at 17:44):Instead of N ≅ N ⊗ P, another alternative is to use a "well-sorted" version of the calculus where each name is labeled with the sort of the names that will be sent over it. That lets us give a unique type to the morphisms x! and x?. It's very much like how untyped lambda calculus is really singly-typed lambda calculus where the one type X ≅ X -> X, but in simply-typed lambda calc everything terminates.
Also, the fact that we're distinguishing x! from x? means we're using polarized names, where you can either send on a name or receive, but not both.
Dan Doel (Apr 22 2020 at 17:52):Is it still not confluent when you do that? (Guessing yes.)
Mike Stay (Apr 22 2020 at 18:00):You are right, it is not confluent.
Mike Stay (Apr 22 2020 at 18:02):I've just remembered that there's a linear pi calculus that Yoshida and Honda described. It sounds like there may be something there that fits better with my diagrams.
Mike Stay (Apr 22 2020 at 18:05):I haven't looked at these diagrams in years because I kept running into problems, but they're so close to working that there must be something there.
Dan Doel (Apr 22 2020 at 18:14):I'm no expert, but it vaguely sounds to me like typed pi calculus could correspond to classical logic. But maybe there's some reason that wouldn't work out. Computational interpretations of classical logic generally lack confluence, though, I think.
Dan Doel (Apr 22 2020 at 18:17):I guess classical logic wouldn't have N and P, though.
Christian Williams (Apr 22 2020 at 18:26):Should concurrency be under "theory" or "practice"? @Mike Stay
Mike Stay (Apr 22 2020 at 18:30):There should be versions for both. Practice would be, e.g. implementations of actor systems, functional reactive programming, specific consensus algorithms, etc. Theory would be the formal semantics (game theoretic, category theoretic, etc), type theory, decidability, axiomatizing the notion of consensus, etc.
Christian Williams (Apr 22 2020 at 18:44):Yeah, there should be.. but so far we're trying to be somewhat conservative with the streams.
How about we start with theory, and we can make practice later?
Mike Stay (Apr 22 2020 at 19:31):Fine by me.
Henry Story (Sep 05 2022 at 13:02):I was wondering what the best model of the pi-calculus was thought to be now. I saw that @John Baez in 2009 blog on the n-cafe The Pi Calculus was looking to see if there was a way to link it to symmetric monoidal categeories. Then later in 2015 @Mike Stay wrote a blog post A 2-Categorical Approach to the Pi Calculus. There is mention of a follow-up to that article, but I could not find it.
I am interested to see how this could help think about actor systems, and indeed model the WWW.
John Baez (Sep 05 2022 at 14:33):@Mike Stay and @Christian Williams were working on that for a while, but as far as I know they've stopped.
Henry Story (Sep 05 2022 at 14:40):I remember watching your (John Baez') introductory talk on symmetric monoidal categories and being struck on the importance of names to link the inputs and the outputs together. I guess that is the mathematical reason for why the actor system akka.io names its actors with URLs.
It should also tie in with the analysis of linked data as a symmetric monoidal category Integrity Constraints for Linked Data where documents have incoming and outgoing links, the URLS name the composition points. And then of course RDF itself is explained in terms of symmetric monoidal categories in Knowledge Representation in Bicategories of Relations.
Great introduction from examples to Symmetric Monoidal Categories by @johncarlosbaez : their use in electrical engineering, quantum theory, programming, logic, ecology and other *open* systems with some thoughts on the 3rd law of thermodynamics. https://www.youtube.com/watch?v=DAGJw7YBy8E&t=18s
- The 🐠 BabelFish (@bblfish)In short: I also feel like there is something essential going on here with symmetric monoidal categories and the web - which feels like an actor system to me .
Christian Williams (Sep 05 2022 at 15:33):Here's A categorical model of an i/o-typed pi calculus just a few years ago.
John Baez (Sep 05 2022 at 15:50):Hmm, they define something they call a 'Freyd category' and give as the simplest example. (A Freyd category is actually a functor between two categories, with some properties.)
John Baez (Sep 05 2022 at 15:51):Part of their formalization uses a 'compact closed Freyd category'. I think some category theorists might set up these ideas a bit differently.
Henry Story (Sep 05 2022 at 17:05):I guess it makes sense that a category that would unite functional programming and indeterministic processes would be one whose simplest example relates Set and Rel... :open_mouth:
image.png
image.png
Henry Story (Sep 05 2022 at 18:45):Ken Sakayori, gave a talk on the paper: "Categorical analysis of the pi-calculus" where he looks at shortcomings of it
https://www.youtube.com/watch?v=dVnbUyT8IMw
Henry Story (Sep 05 2022 at 18:49):That led to the paper Output Without Delay: A π-Calculus Compatible with Categorical Semantics. I am not sure I understand though: they work on a forwarder that does not introduce delays. If a forwarder is a message passing system then I would assume it always introduces delays.
Henry Story (Sep 05 2022 at 18:59):Oh I found a talk by @Christian Williams on pi calculus :-)
https://www.youtube.com/watch?v=NTJBMbTIJis
Tom Hirschowitz (Sep 06 2022 at 07:41):Shameful self-promotion: with @Clovis Eberhart and @Thomas Seiller, we constructed a game model of -calculus, in which strategies are presented as sheaves on a category of plays. The notion of play here means multi-party play, which includes forking (= a player dividing into two players). This is used to model parallel composition in the -calculus. And the coverage essentially says that a play is covered by its sub-views, which are individual histories of players.
Henry Story (Sep 06 2022 at 07:53):As I was looking through the papers by Ken Sakayori yesterday I noticed A Truly Concurrent Game Model of the Asynchronous -Calculus. That seems to have come out at the same time as @Tom Hirschowitz's paper using sheaves. Does the game model of pi-calculus deal with "true concurrency". (I guess that is the concurrency we have one the WWW where things really do happen simultaneously).
Henry Story (Sep 06 2022 at 08:09):Ok, I added your paper @Tom Hirschowitz to my Twitter thread on Actors https://twitter.com/bblfish/status/1567062264926150656
"strategies are presented as sheaves on a category of multi-party play, with forking (= a player dividing into 2) modeling parallel composition in the π-calculus. The coverage says that a play is covered by its sub-views = individual histories of players." https://lmcs.episciences.org/4069 https://twitter.com/bblfish/status/1567062264926150656/photo/1
- The 🐠 BabelFish (@bblfish) Henry Story (Sep 06 2022 at 08:11):Now practically I was hoping this could help me decide when Actors would be the right abstraction to use in programming over FP Effects - such as the Cats FS2 library. But I think it is going to take quite some work to find a way from these abstractions to a coding decision...
Well it is helping in so far as dismissal of Actors on the ground that they are don't have mathematical cats support seem to be on a very weak ground now :-)
Tom Hirschowitz (Sep 06 2022 at 08:17):No, their paper came out two years later... and they don't cite us.
Tom Hirschowitz (Sep 06 2022 at 09:19):To explain a bit more, I think they don't really consider our model to be a game model because our plays do not look like standard, game-semantical plays. @Clovis Eberhart and I later argued that it is a matter of presentation.
Tom Hirschowitz (Sep 06 2022 at 09:21):Oh, and a second reason iirc is that we do not work out the usual "composition+hiding" pattern of game semantics.
Henry Story (Sep 06 2022 at 09:22):Oh very nice :-) Thanks for those pointers.