<p>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 <em>Verifyer</em> and <em>Falsifyer</em> and in second case it is <em>Program</em> and <em>Environment</em>.</p>
<p>Curry-Howard gives correspondence between proofs and programs. This seems very similar to me in multiple ways, so my question is: can <em>Verifyer</em> player be seen as corresponding to <em>Program</em> in some case?</p>
<p>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.</p>

CC BY-SA 4.0
2023-10-04T11:19:12.520Z
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.)
Martin Berger
CC BY-SA 4.0
2023-10-16T13:26:11.060Z
So "innocent strategies" should be related to continuations?
uhbif19
CC BY-SA 4.0
2023-10-16T19:02:47.240Z
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.
Martin Berger
<gt.game-theory><semantics><curry-howard><two-player-games>
Do game semantics for logic have Curry-Howard-like correspondence with game semantics for programming languages?
uhbif19
# Do game semantics for logic have Curry-Howard-like correspondence with game semantics for programming languages?

(Asked by: username_0 on 2023-10-03)

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.

**Tags:** gt.game-theory, semantics, curry-howard, two-player-games

> **Comments:**
> **username_1**: 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.)  
> **username_0**: So "innocent strategies" should be related to continuations?  
> **username_1**: 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.  

---

## 0 answers

