Abstract
Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent’s actions. We thus develop Constructive Game Logic, which extends Parikh’s Game Logic (GL) with constructivity and with first-order programs à la Pratt’s first-order dynamic logic (DL). Our major contributions include: 1. a novel realizability semantics capturing the adversarial dynamics of games, 2. a natural deduction calculus and operational semantics describing the computational meaning of strategies via proof-terms, and 3. theoretical results including soundness of the proof calculus w.r.t. realizability semantics, progress and preservation of the operational semantics of proofs, and Existential Properties on support of the extraction of computational artifacts from game proofs. Together, these results provide the most general account of a Curry-Howard interpretation for any program logic to date, and the first at all for Game Logic.
This research was sponsored by the AFOSR under grant number FA9550-16-1-0288. The authors were also funded by the NDSEG Fellowship and Alexander von Humboldt Foundation, respectively.
Chapter PDF
Similar content being viewed by others
References
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000), https://doi.org/10.1006/inco.2000.2930
Aczel, P., Gambino, N.: The generalised type-theoretic interpretation of constructive set theory. J. Symb. Log. 71(1), 67–103 (2006), https://doi.org/10.2178/jsl/1140641163
Alechina, N., Mendler, M., de Paiva, V., Ritter, E.: Categorical and Kripke semantics for constructive S4 modal logic. In: Fribourg, L. (ed.) CSL. LNCS, vol. 2142, pp. 292–307. Springer (2001), https://doi.org/10.1007/3-540-44802-0_21
Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.J.: Normalization by evaluation for typed lambda calculus with coproducts. In: LICS. pp. 303–310. IEEE Computer Society (2001), https://doi.org/10.1109/LICS.2001.932506
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002), https://doi.org/10.1145/585265.585270
van Benthem, J.: Logic of strategies: What and how? In: van Benthem, J., Ghosh, S., Verbrugge, R. (eds.) Models of Strategic Reasoning - Logics, Games, and Communities, LNCS, vol. 8972, pp. 321–332. Springer (2015), https://doi.org/10.1007/978-3-662-48540-8_10
van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Aiello, M., Pratt-Hartmann, I., van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 217–298. Springer (2007), https://doi.org/10.1007/978-1-4020-5587-4_5
van Benthem, J., Bezhanishvili, N., Enqvist, S.: A propositional dynamic logic for instantial neighborhood models. In: Baltag, A., Seligman, J., Yamada, T. (eds.) Logic, Rationality, and Interaction - 6th International Workshop, LORI 2017, Sapporo, Japan, September 11–14, 2017, Proceedings. LNCS, vol. 10455, pp. 137–150. Springer (2017), https://doi.org/10.1007/978-3-662-55665-8_10
van Benthem, J., Pacuit, E.: Dynamic logics of evidence-based beliefs. Studia Logica 99(1–3), 61–92 (2011), https://doi.org/10.1007/s11225-011-9347-x
van Benthem, J., Pacuit, E., Roy, O.: Toward a theory of play: A logical perspective on games and interaction. Games (2011), https://doi.org/10.3390/g2010052
Bishop, E.: Foundations of constructive analysis (1967)
Bohrer, R., Platzer, A.: Constructive hybrid games. CoRR abs/2002.02536 (2020), https://arxiv.org/abs/2002.02536
Bridges, D.S., Vita, L.S.: Techniques of constructive analysis. Springer (2007)
Celani, S.A.: A fragment of intuitionistic dynamic logic. Fundam. Inform. 46(3), 187–197 (2001), http://content.iospress.com/articles/fundamenta-informaticae/fi46-3-01
Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR. LNCS, Springer (2007), https://doi.org/10.1007/978-3-540-74407-8_5
Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2/3), 95–120 (1988), https://doi.org/10.1016/0890-5401(88)90005-3
Curry, H., Feys, R.: Combinatory logic. In: Heyting, A., Robinson, A. (eds.) Studies in logic and the foundations of mathematics. North-Holland (1958)
Degen, J., Werner, J.: Towards intuitionistic dynamic logic. Logic and Logical Philosophy 15(4), 305–324 (2006). https://doi.org/10.12775/LLP.2006.018
Doberkat, E.: Towards a coalgebraic interpretation of propositional dynamic logic. CoRR abs/1109.3685 (2011), http://arxiv.org/abs/1109.3685
Fernández-Duque, D.: The intuitionistic temporal logic of dynamical systems. Log. Methods in Computer Science 14(3) (2018), https://doi.org/10.23638/LMCS-14(3:3)2018
Frittella, S., Greco, G., Kurz, A., Palmigiano, A., Sikimic, V.: A proof-theoretic semantic analysis of dynamic epistemic logic. J. Log. Comput. 26(6), 1961–2015 (2016), https://doi.org/10.1093/logcom/exu063
Fulton, N., Platzer, A.: A logic of proofs for differential dynamic logic: Toward independently checkable proof certificates for dynamic logics. In: Avigad, J., Chlipala, A. (eds.) CPP. pp. 110–121. ACM (2016). https://doi.org/10.1145/2854065.2854078
Ghilardi, S.: Presheaf semantics and independence results for some non-classical first-order logics. Arch. Math. Log. 29(2), 125–136 (1989), https://doi.org/10.1007/BF01620621
Ghosh, S.: Strategies made explicit in dynamic game logic. Workshop on Logic and Intelligent Interaction at ESSLLI. pp. 74–81 (2008)
Goranko, V.: The basic algebra of game equivalences. Studia Logica 75(2), 221–238 (2003), https://doi.org/10.1023/A:1027311011342
Griffin, T.: A formulae-as-types notion of control. In: Allen, F.E. (ed.) POPL. pp. 47–58. ACM Press (1990), https://doi.org/10.1145/96709.96714
Harper, R.: The holy trinity (2011), https://web.archive.org/web/20170921012554/existentialtype.wordpress.com/2011/03/27/the-holy-trinity/
Hilken, B.P., Rydeheard, D.E.: A first order modal logic and its sheaf models
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259
van der Hoek, W., Jamroga, W., Wooldridge, M.J.: A logic for strategic reasoning. In: Dignum, F., Dignum, V., Koenig, S., Kraus, S., Singh, M.P., Wooldridge, M.J. (eds.) AAMAS. ACM (2005), https://doi.org/10.1145/1082473.1082497
Howard, W.A.: The formulae-as-types notion of construction. To HB Curry: essays on combinatory logic, lambda calculus and formalism 44, 479–490 (1980)
Kamide, N.: Strong normalization of program-indexed lambda calculus. Bull. Sect. Logic Univ. Łódź 39(1–2), 65–78 (2010)
Lipton, J.: Constructive Kripke semantics and realizability. In: Moschovakis, Y. (ed.) Logic from Computer Science. pp. 319–357. Springer (1992). https://doi.org/10.1007/978-1-4612-2822-6_13
Makarov, E., Spitters, B.: The Picard algorithm for ordinary differential equations in Coq. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP. LNCS, vol. 7998. Springer (2013), https://doi.org/10.1007/978-3-642-39634-2_34
Mamouras, K.: Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism. Log. Methods Computer Science 12(3) (2016), https://doi.org/10.2168/LMCS-12(3:6)2016
Mitsch, S., Platzer, A.: ModelPlex: Verified runtime validation of verified cyber-physical system models. Form. Methods Syst. Des. 49(1), 33–74 (2016). https://doi.org/10.1007/s10703-016-0241-z, special issue of selected papers from RV’14
van Oosten, J.: Realizability: A historical essay. Mathematical Structures in Computer Science 12(3), 239–263 (2002), https://doi.org/10.1017/S0960129502003626
Parikh, R.: Propositional game logic. In: FOCS. pp. 195–200. IEEE (1983), https://doi.org/10.1109/SFCS.1983.47
Pauly, M.: A modal logic for coalitional power in games. J. Log. Comput. 12(1), 149–166 (2002), https://doi.org/10.1093/logcom/12.1.149
Pauly, M., Parikh, R.: Game logic - an overview. Studia Logica 75(2), 165–182 (2003), https://doi.org/10.1023/A:1027354826364
Peleg, D.: Concurrent dynamic logic. J. ACM 34(2), 450–479 (1987), https://doi.org/10.1145/23005.23008
Platzer, A.: Differential game logic. ACM Trans. Comput. Log. 17(1), 1:1–1:51 (2015). https://doi.org/10.1145/2817824
Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reas. 59(2), 219–265 (2017). https://doi.org/10.1007/s10817-016-9385-1
Platzer, A.: Uniform substitution for differential game logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR. LNCS, vol. 10900, pp. 211–227. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6_15
Pratt, V.R.: Semantical considerations on floyd-hoare logic. In: FOCS. pp. 109–121. IEEE (1976). https://doi.org/10.1109/SFCS.1976.27
Ramanujam, R., Simon, S.E.: Dynamic logic on games with structured strategies. In: Brewka, G., Lang, J. (eds.) Knowledge Representation. pp. 49–58. AAAI Press (2008), http://www.aaai.org/Library/KR/2008/kr08-006.php
Robinson, J.: Definability and decision problems in arithmetic. J. Symb. Log. 14(2), 98–114 (1949), https://doi.org/10.2307/2266510
The Coq development team: The Coq proof assistant reference manual (2019), https://coq.inria.fr/
Van Benthem, J.: Games in dynamic-epistemic logic. Bulletin of Economic Research 53(4), 219–248 (2001)
Vanderwaart, J., Dreyer, D., Petersen, L., Crary, K., Harper, R., Cheng, P.: Typed compilation of recursive datatypes. In: Shao, Z., Lee, P. (eds.) Proceedings of TLDI’03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, Louisiana, USA, January 18, 2003. pp. 98–108. ACM (2003), https://doi.org/10.1145/604174.604187
Weihrauch, K.: Computable Analysis - An Introduction. Texts in Theoretical Computer Science. An EATCS Series, Springer (2000), https://doi.org/10.1007/978-3-642-56999-9
Wijesekera, D.: Constructive modal logics I. Ann. Pure Appl. Logic 50(3), 271–301 (1990), https://doi.org/10.1016/0168-0072(90)90059-B
Wijesekera, D., Nerode, A.: Tableaux for constructive concurrent dynamic logic. Ann. Pure Appl. Logic (2005), https://doi.org/10.1016/j.apal.2004.12.001
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Bohrer, R., Platzer, A. (2020). Constructive Game Logic. In: Müller, P. (eds) Programming Languages and Systems. ESOP 2020. Lecture Notes in Computer Science(), vol 12075. Springer, Cham. https://doi.org/10.1007/978-3-030-44914-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-44914-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-44913-1
Online ISBN: 978-3-030-44914-8
eBook Packages: Computer ScienceComputer Science (R0)