The Eriskay project homepage
John Longley, School of Informatics, University of Edinburgh, UK
The Eriskay project is an ongoing experiment
in programming language design inspired by game models
of computation.
(If it’s the Scottish island you’re after, try this other
Eriskay homepage.)
Most modern programming languages involve a rich assortment of programming
constructs, often combined in complex ways. However, in many cases,
languages have tended to evolve without any definite guiding principles,
so that the languages turn out more complex than they need to be.
This makes them harder to learn, use, implement and reason about.
In the Eriskay project we are exploring a more principled approach,
by designing a programming language (Eriskay)
based on some recently developed mathematical models
of computation known as game models.
These models exhibit a remarkably rich structure, which has suggested novel
and powerful features to include in our language;
on the other hand, the models’ fundamental simplicity ensures that these features
fit together in a clean and natural way. Moreover, because it is soundly based
in a rich mathematical theory, our language will be very suitable for ongoing
work on proving the correctness of programs.
We have now completed the formal definition
of a language called Lingay.
This is intended as a research language embodying many of the
innovative aspects of Eriskay, and suitable for pedagogical purposes,
metatheoretical study, programming experiments, and case studies in
program verification.
We have also produced a prototype implementation of Lingay
based directly on the underlying game semantics; this pioneers a new approach
to semantics-based language prototyping.
[Disclaimer: Lingay is not itself intended for serious programming
applications!]
The following specific language innovations have arisen from our work so far,
and are embodied in the design of Lingay:
- A system of class types allowing class implementations to be treated as first-class values within a higher-order framework, opening up new possibilities for functorized styles of programming-in-the-large with classes.
- New language primitives for safe coroutining and backtracking, made possible by the underlying linear type system.
- A static type system regulating the use of higher-order store via the notion of argument-safety, offering a new approach to the problem of encapsulating computational effects (e.g. exceptions and other control flow constructs) in the presence of higher-order store.
- A system of encapsulated reference types, supplementing the argument-safety system by providing a mechanism for unrestricted use of higher-order store, without sacrificing semantic simplicity or the benefits of argument-safety.
- A novel ‘virtual’ treatment of field access and update within imperative-style method implementations.
- A system of linear classes, suitable for objects whose state is not freely copyable (these admit simpler reasoning principles than ordinary objects).
In the future, we plan to extend Lingay with additional features to yield
Eriskay –
a full-scale language suitable for real programming applications.
We also plan to use Lingay and its implementation
as a platform for experimenting with programming idioms made
possible by our new language features, and for case studies in reasoning about programs.
- J. Longley,
Definition of the Lingay programming language (Version 0.2),
41 pages (pdf).
Published as Informatics Research Report EDI-INF-RR-1283,
University of Edinburgh (2008).
- J. Longley and N. Wolverson,
Eriskay: a programming language based on game semantics.
An earlier version (pdf),
now rather out-of-date in content,
was presented at the GaLoP III workshop, ETAPS 2008, Budapest.
A thoroughly updated version will be available here soon – this will be the
place to start if you're interested in the main ideas that have resulted
from the project.
- N. Wolverson,
Game semantics for an object oriented language,
210 pages (pdf).
PhD thesis, School of Informatics, University of Edinburgh.
Examined May 2008; final version approved December 2008.
This work lays many of the theoretical foundations that have undergirded
the design of Lingay.
- J. Longley,
Interpreting localized computational effects using operators of
higher type, 14 pages
(pdf).
In A. Beckmann, C. Dimitracopoulos and B. Loewe (editors),
Logic and Theory of Algorithms, Fourth Conference on
Computability in Europe, CiE 2008, Athens, proceedings,
Springer LNCS 5028 (2008).
This explains the theoretical idea behind our treatment of ‘awkward’
features such as unrestricted higher order store and references with equality testing.
The prototype implementation, by John Longley and Nicholas Wolverson,
runs on SML of New Jersey (at least on the last stable version, 110.0.7 –
let us know if you have problems running it on more recent versions).
Just fetch this tarfile, unpack it
using an incantation such as tar -xf LingayImpl2.tar,
and follow the instructions in the README file (which also contains details
of a few features not yet implemented).
Alternatively, browse the source files here.
Here is some sample Lingay code consisting
of a few class definitions (a more illuminating set of tutorial examples will appear here soon).
Here is some more Lingay code giving
implementations of certain crucial operations important to the metatheory of Lingay
(not recommended for beginners!).
- Most of this research to date has been funded by EPSRC grant
GR/T08791/01
‘A programming language based on game semantics’,
which ran from April 2005 to May 2008.
- Article and discussion on Eriskay on the
Lambda the Ultimate weblog.
- Slides from John Longley's talk on Eriskay at
the Scottish Programming Languages Seminar (Glasgow, October 2008).
- Some slides from Nicholas Wolverson's
talk on Eriskay at the GaLoP III workshop (Budapest, April 2008).
Some more slides from his earlier talk
at the GaLoP II workshop (Seattle 2006).
John Longley
Last modified: Wed May 13 12:41:26 BST 2009