Algorithmic Game Semantics and Static Analysis

Abstract

Game Semantics has been developed over the past 12 years or so as a dist inctive approach to the semantics of programming language. It is composit ional in the tradition of denotational semantics, and has led to the cons truction of fully abstract models for programming languages incorporating a wide variety of features which have proved resistant to more tradition al approaches, including (combinations of): higher-order procedures, loca lly scoped variables and references, non-local control operators, non-det erminism, probability, concurrency and more. At the same time, game seman tics has a concrete aspect: programs are interpreted as strategies for ce rtain two-player games, and these strategies can be represented by automa ta. This algorithmic aspect of game semantics has been developed over the past few years, by Dan Ghica, Luke Ong, Andrzej Murawski and the present author. This has led to a novel approach to compositional model-checking and static analysis. We will survey some of the work which has been done , and discuss some directions for future research in this area.