Category Theory
Zulip Server
Archive

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.

Stream: deprecated: game semantics

Topic: stream events

Notification Bot (Apr 12 2020 at 02:44):

Stream created by Faré.

Henry Story (Apr 12 2020 at 07:10):

The 2018 book Immanent Reasoning or Equality in Action gives a very clearly worked out game semantics for Constructive Type Theory with dependent types, which requires thinking of two players one putting forward a thesis and the other trying to disprove it. It would be very interesting to develop this to HoTT. It would also be really interesting to find something that develops the material proofs side more.

Faré (Apr 24 2020 at 18:48):

Questions for @Paul-André Melliès after his talk:

Your slide of typing rules for simple lambda calculus had two colors—what do they mean?
in your ordering of negations as a strategy—shouldn't one player's strategy be independent from the other? how can you know the order that the other will choose? Or does the diagram work despite that? There's something I'm missing. Where can I learn more about those 3d string diagrams in the context of game semantics?

Faré (Apr 24 2020 at 18:49):

or do your diagrams correspond to "one play of the game" vs whether the proponent has a winning strategy?

Faré (Apr 24 2020 at 19:05):

Also, a question I have: does game semantics somehow generalize both Curry-Howard isomorphism (from proofs, propositions to terms, types) and the Russell-Whitehead isomorphism (from traces, terms to proofs, terms) ?

Faré (Apr 24 2020 at 19:10):

in the scheduling diagram, it was not initially obvious that (1) the tuples of +/- in your commutative diagram were vertical in the string diagram. And then, it was not clear what the two colors meant.

Faré (Apr 24 2020 at 19:13):

Also, my zoom was cut while you were explaining the "key observation", so now I don't have the key :-(

Faré (Apr 24 2020 at 19:25):

What left me hungry in your talk: I have sufficient understanding of game semantics and linear logic, but insufficient understanding of category theory, and there are a lot of things that were more suggestive than explanatory for me, lacking this background.

Faré (Apr 24 2020 at 19:26):

Your describing functors at "dimension 0, 1, 2" looked very promiseful, but I don't understand how to give it a formal meaning (it doesn't help that I got bounced on and off of zoom)

Faré (Apr 24 2020 at 19:40):

finally, your presentation mentions differential linear logic, but I completely missed the "differential" part.

Faré (Apr 24 2020 at 19:43):

Are your slides online? Do you have URLs to the papers you recommend to read and/or to even more elementary papers to read about all these topics? Especially from the point of view of someone passably familiar with games but not with category theory.

Faré (Apr 24 2020 at 19:53):

The summarizing of things into dimension 0 look particularly interesting, but it's not clear how you determine which positions are "accepted" or not in which operator.

Notification Bot (Oct 20 2023 at 15:17):

Nathanael Arkor changed the access permissions for this stream from Public to Web-public.

Notification Bot (Oct 31 2023 at 11:20):

Matteo Capucci (he/him) changed the posting permissions for this stream:

Old permissions: All stream members can post.
New permissions: Only organization administrators and moderators can post.

Notification Bot (Oct 31 2023 at 11:20):

Matteo Capucci (he/him) changed the description for this stream.

Old description:

Game Semantics in Category Theory

New description:

Deprecated, use #theory: applications instead. Game Semantics in Category Theory

Notification Bot (Oct 31 2023 at 11:20):

Matteo Capucci (he/him) renamed stream theory: game semantics to deprecated: game semantics.