Clovis Eberhart
ABSTRACT
Game semantics is a rich and successful class of denotational models for programming languages. Most game models feature a rather intuitive setup, yet surprisingly difficult proofs of such basic results as associativity of composition of strategies. We seek to unify these models into a basic abstract framework for game semantics, game settings. Our main contribution is the generic construction, for any game setting, of a category of games and strategies. Furthermore, we extend the framework to deal with innocence, and prove that innocent strategies form a subcategory. We finally show that our constructions cover many concrete cases, mainly among the early models [5, 23] and the recent, sheaf-based ones [40].
- IEEE 1997. Proc. 12th Symposium on Logic in Computer Science IEEE.Google Scholar
- IEEE 2015. Proc. 30th Symposium on Logic in Computer Science IEEE.Google Scholar
- S. Abramsky. 2003. Sequentiality vs. Concurrency In Games And Logic. Mathematical Structures in Computer Science 13, 4 (2003), 531--565. Google ScholarDigital Library
- S. Abramsky, K. Honda, and G. McCusker. 1998. A Fully Abstract Game Semantics for General References. In Proc. 13th Symposium on Logic in Computer Science IEEE, 334--344. Google ScholarDigital Library
- S. Abramsky, R. Jagadeesan, and P. Malacaria. 2000. Full Abstraction for PCF. Information and Computation 163, 2 (2000), 409--470. Google ScholarDigital Library
- P. Baillot, V. Danos, T. Ehrhard, and L. Regnier. 1997. Believe it or not, AJM's Games Model is a Model of Classical Linear Logic, See {1}, 68--75. Google ScholarDigital Library
- A. Blass. 1972. Degrees of indeterminacy in games. Fundamenta Mathematica LXXVII (1972), 151--162.Google Scholar
- A. Blass. 1992. A game semantics for linear logic. Annals of Pure and Applied Logic 56, 1-3 (1992), 183--220.Google ScholarCross Ref
- N.J. Bowler. 2011. A unified approach to the construction of categories of games. Ph.D. Dissertation. University of Cambridge.Google Scholar
- S. Castellan, P. Clairambault, and G. Winskel. 2015. The parallel intensionally fully abstract games model of PCF, See {2}.Google Scholar
- C. Eberhart and T. Hirschowitz. 2017. Game semantics as a singular functor, and definability as geometric realisation. (2017). Preprint hal-01527171.Google Scholar
- C. Eberhart and T. Hirschowitz. 2017. What's in a game? A theory of game models. (2017). Preprint hal-01634162.Google Scholar
- M. P. Fiore. 2012. Discrete Generalised Polynomial Functors - (Extended Abstract). In Proc. 39th International Colloquium on Automata, Languages and Programming (LNCS), Vol. 7392. Springer, 214--226. Google ScholarDigital Library
- R. H. G. Garner and T. Hirschowitz. 2018. Shapely monads and analytic functors. Journal of Logic and Computation 28, 1 (2018), 33--83.Google ScholarCross Ref
- R. Guitart. 1980. Relations et carrés exacts. Annales des Sciences Mathématiques du Québec 4, 2 (1980), 103--125.Google Scholar
- R. Harmer. 1999. Games and Full Abstraction for Nondeterministic Languages. Ph.D. Dissertation. Imperial College, University of London.Google Scholar
- R. Harmer, J. M. E. Hyland, and P.-A. Melliès. 2007. Categorical Combinatorics for Innocent Strategies. In Proc. 22nd Symposium on Logic in Computer Science IEEE, 379--388. Google ScholarDigital Library
- R. Harmer and G. McCusker. 1999. A Fully Abstract Game Semantics for Finite Nondeterminism. In LICS. IEEE, 422--430. Google ScholarDigital Library
- F. Hatat. 2013. Graphical games and proof theory. Ph.D. Dissertation. Université de Grenoble.Google Scholar
- M. Hirschowitz. 2004. Jeux abstraits et composition catégorique. Ph.D. Dissertation. Université Paris-Diderot - Paris VII.Google Scholar
- M. Hirschowitz, A. Hirschowitz, and T. Hirschowitz. 2007. A theory for game theories. In Proc. 27th Foundations of Software Technology and Theoretical Computer Science (LNCS), Vol. 4855. Springer, 192--203. Google ScholarDigital Library
- T. Hirschowitz. 2014. Full abstraction for fair testing in CCS (expanded version). Logical Methods in Computer Science 10, 4 (2014).Google Scholar
- J. M. E. Hyland and C.-H. L. Ong. 2000. On Full Abstraction for PCF: I, II, and III. Information and Computation 163, 2 (2000), 285--408. Google ScholarDigital Library
- A. Joyal. 1977. Remarques sur la théorie des jeux à deux personnes. Gazette des Sciences Mathématiques du Québec 1, 4 (1977), 46--52.Google Scholar
- A. Joyal. 1986. Foncteurs analytiques et espèces de structure. In Combinatoire énumérative (Montréal 1985) (Lecture Notes in Mathematics), Vol. 1234. Springer, 126--159.Google Scholar
- J. Laird. 1997. Full Abstraction for Functional Languages with Control, See {1}, 58--67. Google ScholarDigital Library
- S. Mac Lane. 1998. Categories for the Working Mathematician (2nd ed.). Number 5 in Graduate Texts in Mathematics. Springer.Google Scholar
- G. McCusker. 1996. Games and Full Abstraction for a Functional Metalanguage with Recursive Types. Ph.D. Dissertation. Imperial College, University of London.Google Scholar
- G. McCusker. 2000. Games and Full Abstraction for FPC. Information and Computation 160, 1-2 (2000), 1--61.Google ScholarCross Ref
- G. McCusker, J. Power, and C. Wingfield. 2012. A Graphical Foundation for Schedules. In Proc. 28th Conf. on the Math. Found. of Prog. Semantics (Electronic Notes in Theoretical Computer Science), Vol. 286. Elsevier, 273--289. Google ScholarDigital Library
- P.-A. Melliès. 2004. Asynchronous games 2: the true concurrency of innocence. In Proc. 15th International Conference on Concurrency Theory (LNCS), Vol. 3170. Springer, 448--465.Google ScholarCross Ref
- P.-A. Melliès. 2005. Asynchronous Games 4: A Fully Complete Model of Propositional Linear Logic. In Proc. 20th Symposium on Logic in Computer Science IEEE, 386--395. Google ScholarDigital Library
- P.-A. Melliès. 2012. Game Semantics in String Diagrams. In Proc. 27th Symposium on Logic in Computer Science IEEE, 481--490. Google ScholarDigital Library
- P.-A. Melliès and S. Mimram. 2007. Asynchronous Games: Innocence Without Alternation. In Proc. 19th International Conference on Concurrency Theory (LNCS), Vol. 4703. Springer, 395--411. Google ScholarDigital Library
- A. S. Murawski and N. Tzevelekos. 2016. Nominal Game Semantics. Foundations and Trends in Programming Languages 2, 4 (2016), 191--269. Google ScholarDigital Library
- H. Nickau. 1994. Hereditarily Sequential Functionals. In Proc. Logical Foundations of Computer Science (LNCS), Vol. 813. Springer, 253--264. Google ScholarDigital Library
- S. Rideau and G. Winskel. 2011. Concurrent Strategies. In Proc. 26th Symposium on Logic in Computer Science IEEE, 409--418. Google ScholarDigital Library
- E. Riehl. 2014. Categorical Homotopy Theory. Number 24 in New Mathematical Monographs. Cambridge University Press.Google Scholar
- T. Tsukada and C.-H. L. Ong. 2014. Innocent Strategies are Sheaves over Plays---Deterministic, Non-deterministic and Probabilistic Innocence. (2014). arXiv:cs/1409.2764Google Scholar
- T. Tsukada and C.-H. L. Ong. 2015. Nondeterminism in Game Semantics via Sheaves, See {2}.Google Scholar
- M. Weber. 2004. Generic morphisms, parametric representations and weakly cartesian monads. Theory and Applications of Categories 13 (2004), 191--234.Google Scholar
- M. Weber. 2007. Familial 2-functors and parametric right adjoints. Theory and Applications of Categories 18, 22 (2007), 665--732.Google Scholar
Index Terms
- What's in a game?: A theory of game models
Recommendations
Categorical combinatorics of scheduling and synchronization in game semantics
Game semantics is the art of interpreting types as games and programs as strategies interacting in space and time with their environment. In order to reflect the interactive behavior of programs, strategies are required to follow specific scheduling ...
Innocent game models of untyped λ-calculus
Special issue on theories of types and proofsWe present a new denotational model for the untyped &lgr;-calculus, using the techniques of game semantics. The strategies used are innocent in the sense of Hyland and Ong (Inform. and Comput., to appear) and Nickau (Hereditarily Sequential Functionals: A ...
Refinement-Based Game Semantics for Certified Abstraction Layers
LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceFormal methods have advanced to the point where the functional correctness of various large system components has been mechanically verified. However, the diversity of semantic models used across projects makes it difficult to connect these component to ...
Comments