Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I was going to start game semantics to record a couple of references to dependent type theory, but I’m getting an error message at the moment. So I’ll just leave here for now:
In logic, game semantics is used to provide a semantic interpretation of logic constructions in terms of strategies for opposing players to win a game corresponding to some proposition.
For attempts to formulate a game semantics for dependent type theory, see
Matthijs Vakar, Radha Jagadeesan, Samson Abramsky, Game Semantics for Dependent Types, (pdf)
Norihiro Yamada, _Game Semantics for Martin-Löf Type Theory, (arXiv:1610.01669)
David, it seems to be working now (for me).
… or was the error message on trying to submit the form. Something about Javascript and cookies.
There is a nontrivial amount of game semantics literature in linear logic. One must not fail to mention Joyal’s short paper on games and compact closed categories, for example, with many refinements (I believe for example Hyland and Ong have looked at this for some variant of multiplicative linear logic).
At some point in the past I had a project on game semantics to solve a problem arising in coherence theory for symmetric monoidal closed categories, and Jim Dolan and I had worked out some game semantics for cartesian closed categories (his “holodeck games”).
Re #3, yes it was about Javascript and cookies. All seems fine now.
Re #4, Todd, do you mean
I’m sure there’s plenty more to add.
I’m pretty sure that’s the one, yes. My memory is that it was published in the Canadian Comptes Rendus.
I added reference to a translation of it by Robin Houston.
1 to 8 of 8