Details of Grant 

EPSRC Reference:	EP/E016146/1
Title:	Relational Parametricity for Computational Effects
Principal Investigator:	Simpson, Professor A
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Lab. for Foundations of Computer Science
Organisation:	University of Edinburgh
Scheme:	Standard Research
Starts:	01 October 2006	Ends:	30 September 2007	Value (£):	51,766
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
Mathematically, a computer program may be thought of as a function that maps possible inputvalues to the associated output values computed by the program. However, this is too simplistic.In reality, programs perform additional non-functional behaviour . For example,they modify the store, make nondeterministic choices, cause errors, etc. Collectively, such non-functional behaviours are called computational effects .Polymorphism is an important device in programming that allows a programto be used for many different types of input and output, rather than for justa single type. Christopher Strachey coined the term parametric polymorphism to describe polymorphic programs that apply the same uniform algorithm acrossall types of input. In 1983, John Reynolds proposed that Strachey's notionof parametricity could be modeled by a mathematical property asserting thatpolymorphic programs should preserve certain relations between data of different types. This notion of relational parametricity has since proved itself tobe very useful. In particular, it provides a powerful and useful principle for proving behavioural equivalences of programs.The notion of relational parametricity, as formulated by Reynolds, relies on theassumption that programs are functions. The goal of the proposed researchis to study a generalized notion of relational parametricity that appliesto programs that perform effects.Our research will build on a simple metalanguage for parametric polymorphism with effects recently proposed by the principal investigator. The metalanguagewill be used as the basis for developing principles for reasoning about parametricity in the presence of effects. Such principles will be presented in a formal logic.The metalanguage will also be used as a target language for the translation ofdifferent evaluation mechanisms for polymorphism, allowing the transfer ofthe reasoning principles to realistic programming mechanisms. Finally, weshall study instances of our metalanguage and logic in the context ofparticular computational effects of interest, such as probabilistic choiceand so-called continuations (jumping mechanisms).
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.ed.ac.uk