Flow analysis: Games and nets

This paper presents a graph-based formulation of control-flow analysis using results from game semantics and proof-nets. Control-flow analysis aims to give a conservative prediction of the flow of control in a program. In our analysis, terms axe represented by proof-nets and control-flow analysis amounts to the analysis of computation paths in the proof-net. We focus on a context free analysis known in the literature as 0-CFA, and develop an algorithm for the analysis. The algorithm for 0-CFA performs dynamic transitive closure of a graph that is based on the judgement associated with the proof-net. Correctness of the algorithm relies on the correspondence between proof-nets and certain kinds of strategies in game semantics