University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Eriskay: a programming language based on game semantics.

Eriskay: a programming language based on game semantics.

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Sam Staton.

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)

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity