Eriskay: a Programming Language Based on Game Semantics

Eriskay: a Programming Language Based on Game Semantics. John Longley and Nicholas Wolverson. GaLoP 2008.

We report on an ongoing project to design a strongly typed, 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. We describe a simple-minded game model with a rich mathematical structure, and explain how this model may be used to guide the design of our language. We then focus on three specific areas where our approach appears to offer something new: linear types and continuations; observational equivalence for class types; and static control of the use of higher-order store.

In a substantial appendix, we present the formal definition of a fragment of our language which embodies many of the innovative features of the full language.

It's always interesting to see a new programming language strongly based on some mathematical formalism, because a language gives you a concrete example to match the abstract semantic definitions to, and game semantics is something that I've been curious about for a while.

One particularly interesting feature is that the core language has a restricted model of the heap, which controls the use of higher-order store in such a way that cycles are prohibited. This is enforced with a notion called "argument safety", which essentially prohibits storing values of higher type into fields which come from "outside" the object. This is somewhat reminiscent of the ownership disciplines found in OO verification systems like Boogie, which enforce a tree structure on the ownership hierarchy. It would be very interesting to find out whether this resemblance is a coincidence or not.

(Samson Abramsky has some lecture notes on game semantics for the very curious.)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I dislike these kinds of

I dislike these kinds of papers because they always lack even toy examples. The idea is intriguing, but whats the pay-off? What kind of code could I expect to write with the language? Programming languages are meant for coding, so at least some coding should be presented lest this just be an exercise in formal semantics.

Region-based resource management

I admit I haven't read the paper yet. I'll try and do that tomorrow. But the description of this restricted heap is quite reminiscent of region-based resource management (in this case, memory). Am I wrong ? If not, that's something which I believe can be enforced through types with effects in functional languages.

Games and regions

Luke Ong and Will Greenland investigated using game semantics to show correctness of region allocation a few years back, so this supports what you say. I understand that the technique leads to much simplified correctness arguments.

The Eriskay paper doesn't cite Will Greenland's DPhil thesis, Games semantics and region analysis (.ps.gz), which was awarded in 2004. I haven't read it.

Link is broken. I couldn't

Link is broken. I couldn't find anything via google for that title either. Anyone else have a link?

Patience

Just wait. web.comlab.ox.ac.uk seems to be down at the moment, though the other comlab domains seem to be working fine. I could send you the file, but coincidentally my mail server isn't working at the moment...

By broken, I mean it returns

By broken, I mean it returns a 404, not that it can't contact the server.

Email

I tried to send the file to you, but I've got the 5 day timout on the address (sconcat "smagi@" "naasking." "homeip.net"). Where should I send it, if you still want it?

Oh, thanks! That's a really

Oh, thanks! That's a really old address actually. I guess you found it via google. You can send it to naasking at gmail dot com.

Eriskay code examples

I apologize for the lack of code examples at present. The paper in
question was written for a game semantics workshop and is targeted
at a fairly theoretical audience. I hope to write some more practically
oriented papers once the language definition has stabilized a bit.
Also, I expect a prototype implementation of at least a fragment of
the language to be made available within the next couple of months,
along with some code examples.

Meanwhile, the comments on things which the argument-safety idea of
Eriskay seems to resemble are very useful - I'll try to follow up
some of these leads.

Thanks for posting! I have

Thanks for posting!

I have a question about how the semantics of heaps works in your language. Do you have to restrict all reference types to the extended language, or can you add first-order reference types to the core language without breaking anything?

The reason I ask comes from the following bit of SML code:

  datatype list = L of list' ref
  and     list' = Nil | Cons of int * list

  let lst = L(ref Nil)

  let val L(r) = lst 
  in 
    r := Cons(5, lst)  (* Now we have a cyclic list *)
  end

Here, we have what naively seems to be a mutable list with only first-order stuff in it, but which does create a cycle.

Reference types

That's a nice example. Strictly speaking, we don't have first order reference types in the core language - and your example suggests it might be difficult to allow them. What we do have is store cells for ground types: essentially, for any ground type t one can create objects with methods
get : unit -> t
put : t -> unit

Note, however, that these store cells are not themselves of ground type, so the analogue of your recursive type definition using store cells would no longer result in a ground type.

This, I think, gives some insight into exactly what additional power is given by reference types in Eriskay: it's not so much the ability to store things (we already have that in the core language) as a kind of aliasing or level of indirection allowing higher order data to be treated as first order (and so, in a sense, treat cyclic structures as acyclic ones).

Semantic Examples

I think you claimed mostly that Eriskay will give you much nicer ways of reasoning about programs that look fairly ordinary, rather than giving you radically new ways to write programs.

If that is correct I think the best examples would prove some interesting property of a program, or safety of a transformation, especially in where denotational semantics doesn't work so well. I don't understand the game semantics enough to prove it myself yet, but it seems like hoisting memory allocation out of a loop might be the sort of thing you could handle nicely.