Home > lambdatheultimate > Imperative Programs as Proofs via Game Semantics

Imperative Programs as Proofs via Game Semantics

April 13th, 2011 04:28 admin Leave a comment Go to comments

Imperative Programs as Proofs via Game Semantics, Martin Churchill, James Laird and Guy McCusker. To appear at LICS 2011.

Game semantics extends the Curry-Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. We can embed intuitionistic ?rst-order linear logic into this system, as well as an imperative total programming language. The logic makes explicit use of the fact that in the game semantics the exponential can be expressed as a ?nal coalgebra. We establish a full completeness theorem for our logic, showing that every bounded strategy is the denotation of a proof.

This paper increases the importance of gaining a more-than-casual understanding of game semantics for me, since it combines two of my favorite things: polarized type theories and imperative higher-order programs.

Source: Imperative Programs as Proofs via Game Semantics

Related Articles:

  1. An operational and axiomatic semantics for non-determinism and sequence points in C
  2. An operational and axiomatic semantics for non-determinism and sequence points in C
  3. An operational and axiomatic semantics for non-determinism and sequence points in C
  4. An operational and axiomatic semantics for non-determinism and sequence points in C
  5. An operational and axiomatic semantics for non-determinism and sequence points in C
blog comments powered by Disqus
YOYOYOOYOYOYO