Imperative Programs as Proofs via Game Semantics