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.