Lambda the Ultimate

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 first-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 final 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.

Redhat has apparently unveiled a new JVM language. Slides here and here. I've got a plane to catch so can't do a proper post, but thought some might be interested. There is nothing more fun than tearing apart someone else's language design, right?

I've been doing some research lately on the various compilation phases. I figured it's not a bad idea, given I'm writing a compiler framework. One topic that I've found interesting of late is Dead Code Analysis. Into that, I've noticed there are two areas of interest:

1. Flow control analysis to detect which branches are living and which are dead: wherein the condition is whether the branch can be reached or not.
2. Live Variable Analysis to detect which variables may be potentially read during one of the live branches within the code.

The question I have is has there been any research related to a wider scope dead code analysis, which involves a broader scope analysis on the entire program. A live analysis done on the members of the program, based upon what delineates a member as living. In some cases if the program is intended to be stand-alone, unused portions, even those public, can be considered dead, in class libraries accessibility modifiers delineate their live status. Once the scope is defined, you can then analyze the internals of the program to determine which parts of the program are needed and which are not. The question then becomes: is the analysis worth the effort?

Insight welcome