  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 a 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 Existence
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.
