Ian Stark

Reasoning with Names and Identity in Programming Languages

EPSRC project grant GR/R04430/01

Laboratory for Foundations of Computer Science
School of Informatics
The University of Edinburgh

Award duration: 2001 - 2004
Award value: £63,625

This is a project carrying out research into reasoning about functional and object-oriented programming languages. The principal investigator is Ian Stark, and the project student is Uli Schöpp.

Reasoning with names: Abstract and slides from a talk at the Oxford University Computing Laboratory, November 2003.

Project outline

This research aims to refine and extend some existing methods for reasoning about programming languages that combine imperative and functional features. Its particular focus is the notion of generativity: the idea that an entity may be freshly created, distinct from all others. This is captured by the study of names, abstract individuals with identity but nothing else: all one can do is generate them, pass them around, and compare them with each other.

There are three principal objectives:

• To implement rule-based reasoning about names in the Coq proof assistant.
• To construct a scheme of rules for reasoning about state in functional languages, based on existing operational methods.
• To develop operational methods for reasoning about local state in a simple object-oriented language, drawing on analogous work with functional languages.

The full project description provides background material and further details.

Page last modified: Tuesday 5 August 2008