Lambda the Ultimate

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 find anything via google for that title either. Anyone else have a link?

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 a 404, not that it can't contact the server.

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 old address actually. I guess you found it via google. You can send it to naasking at gmail dot com.

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.

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).

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.