Both for logic and PLs do have notion of game semantics. Both are defined by two-player dialogue game, but players are different. In first case it is game between Verifyer and Falsifyer and in second case it is Program and Environment.

Curry-Howard gives correspondence between proofs and programs. This seems very similar to me in multiple ways, so my question is: can Verifyer player be seen as corresponding to Program in some case?

One potential problem I see immediately is that logic game semantics is applicable to classic logic, but one can look only on constructive sub case first.

  • 1
    $\begingroup$ You can give game semantics to all manner of programming languages, including those that do not correspond to constructive logics. However, the strategies you need in this case are no longer as well-structured. (They are no longer "innocent strategies" in the terminology of Hyland/Ong.) $\endgroup$ Oct 4, 2023 at 11:19
  • $\begingroup$ So "innocent strategies" should be related to continuations? $\endgroup$
    – uhbif19
    Oct 16, 2023 at 13:26
  • 1
    $\begingroup$ Innocent strategies correspond exactly to the bracket-like nesting of function call and return that you have in pure functional programming. If the language you are modelling is no longer a pure functional, the bracketing is no longer simple (or at all). I suggest to think of a game in terms of multiple players interacting by exchanging messages, that's much more natural than thinking about continuations. $\endgroup$ Oct 16, 2023 at 19:02


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.