Abstract

I will describe an ongoing project to design a class-based object oriented language based around ideas from game semantics. Part of our goal is to create a powerful modern programming language whose clean semantic basis renders it amenable to work in program verification; however, we argue that our semantically inspired approach also yields benefits of more immediate relevance to programmers, such as expressive new language constructs and novel type systems for enforcing security properties of the language.

Our work is based on a simple game model due to Lamarche, when endowed with a suitable linear exponential, suffices for modelling stateful objects, higher order functions, coroutining, recursive types, polymorphism with subtyping, a class system with inheritance and dynamic binding, and even – seen in a certain light – such features as fresh name generation and higher-order store. I will explain in general terms how this model may be used to guide the design of a language, and will then focus on three specific areas where our approach appears to offer something new:

(1) Linear types and coroutining operators. (2) Static control of the use of higher-order store, and how this helps with the encapsulation of computational effects such as exceptions. (3) Higher order programming with classes, including a full abstraction result for class implementations.

(Joint work with Nicholas Wolverson)