|
| EPSRC Reference: |
GR/T08791/01 |
| Title: |
A programming language based on game semantics |
| Principal Investigator: |
Dr JR Longley |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
First Grant Scheme |
| Starts: |
01 April 2005 |
Ends: |
31 May 2008 |
Value (£): |
115,683
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
Most modern programming languages involve a rich assortment of programming constructs, often combined in complex ways. However, there is a tendency for designers of languages simply to "add features" without any particular guiding principles, so that languages sometimes turn out more complex than they need to be. This makes them harder to learn, use, implement and reason about.
We will explore a more principled approach, by designing a language based on some recently developed mathematical models of computation. These models exhibit a remarkably rich structure, which will suggest novel and powerful features to include in our language; on the other hand, the models' fundamental simplicity will ensure that these features fit together in a clean and natural way.In particular, our models will inspire innovative kinds of type systems, which will ensure that certain errors will never occur when programs are run, and allow increased opportunities for faster execution of programs. Moreover, because of its sound logical basis, our language will be very suitable for work on proving the correctness of programs.
Specifically, we will explore the relevant structure of our models, develop a formal definition of our language, and produce a simple prototype implementation.
|
| Final Report Summary |
Most modern programming languages involve a rich assortment of programming constructs, often combined in complex ways. However, there is a tendency for designers of languages simply to "add features" without any definite guiding principles, so that languages sometimes turn out more complex than they need to be. This makes them harder to learn, use, implement and reason about.
In this project we have explored a more principled approach,
by designing a language 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.
In particular, we have undertaken a theoretical investigation of the connections between game models and object oriented languages (the principal research output from this part of the project being the recently defended PhD thesis of Wolverson). On the basis of this experience, we have designed a higher-order class-based object oriented language called Lingay, for which we have provided a detailed 41-page formal definition. A working prototype implementation for most of the language, based directly on an
animation of the underlying game semantics, is also freely available from the project homepage.
The following specific language innovations have arisen from our work, and are embodied in the design of Lingay:
* Powerful new language primitives for coroutining and backtracking, made possible by the underlying linear type system.
* A system of "linear classes", suitable for objects whose state is not freely copyable (these admit simpler reasoning principles than ordinary objects).
* A static type system regulating the use of higher-order store via the notion of "argument-safety", offering a new approach to the well-known problem of encapsulating computational effects (e.g. exceptions) 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 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.
* A novel "virtual" treatment of field access and update within imperative-style method implementations.
An expository report, complementing the formal definition with an informal explanation of the language - its motivations, semantic underpinnings, and main features - is nearing completion and is expected to form the basis for a substantial journal publication.
In the future, we plan to extend Lingay with additional convenience features to yield a full-scale language (called Eriskay) suitable for real programming applications. In the meantime, Lingay and its implementation already provide a platform suitable for future work in program verification, and for experimentation into the programming idioms made possible by our new language features.
In addition, we have completed a major journal publication on computable functionals, consolidating ideas developed in earlier
EPSRC-funded research. This relates to the present project in that it identifies the class of total functionals computable in Lingay and many key sublanguages thereof. Finally, some progress has been
made on the use of resource-aware type systems (similar in spirit
to that of Lingay) to guarantee bounds on the memory usage of
programs; we expect these ideas to be applicable to Lingay itself
in the future.
|
| Further Information: |
|
| Organisation Website: |
http://www.ed.ac.uk |
|
|