Game Semantics and Memory Management Seminars/Workshops

Abstract

Game semantics is an approach to the semantics of programming languages using intuitive game playing ideas. A computation is viewed as a play or an interaction between two players, called Proponent (= Programmer) and Opponent (= Environment), each following a specific strategy. The program in question is the strategy employed by the Proponent, which is set against an Opponent strategy given by the program context. Game semantics was used in 1994 to construct the first syntax-independent fully abstract model of PCF, thus solving a well-known open problem in the Semantics of Computation. The first part of the talk introduces the (fully abstract) game model of PCF, and surveys recent results in game semantics.

The second part is about a memory management model based on regions (Tofte and Talpin 1994), and its connexions with game semantics. A region is a stack of unbounded size. In this approach, the memory is a (horizontally growing) stack of regions; each region grows (vertically) as the computation unfolds until the region in its entirety is popped off the stack. A region inference algorithm, in the form of a type and effect system (in the sense of Gifford and Jouvelot), automatically annotates a program with constructs that explicitly allocate and deallocate memory for values (which may include recursive data structures and function closures). In the purest form of the regions model, no heap memory is needed, and hence there is no need for any garbage collection. An important question of both theoretical and practical interest is the soundness of the type and effect system: whenever a region is deallocated, all values in it are guaranteed to be of no consequence to the rest of the computation. Soundness proofs of this kind are often complex. We apply game semantics to give an abstract view of regions, and use it to interpret the type and effect system. As a consequence we obtain a mple and we hope intuitive soundness proof.