Details of Grant 

EPSRC Reference:	EP/J010995/1
Title:	Unifying Theories of Generic Programming
Principal Investigator:	Hinze, Professor RTW
Other Investigators:	Gibbons, Professor J
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	University of Oxford
Scheme:	Standard Research
Starts:	01 February 2012	Ends:	31 July 2015	Value (£):	574,865
EPSRC Research Topic Classifications:	Fundamentals of Computing Software Engineering
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 07 Dec 2011 EPSRC ICT Responsive Mode - Dec 2011 Announced 26 Oct 2011 EPSRC ICT Responsive Mode - Oct 2011 Deferred
Summary on Grant Application Form
The world is increasingly dependent on robust, reliable software that meets its specification. At the same time, software has to be delivered at an increasingly faster rate. As a consequence, the software industry, especially in Europe and the UK, is facing a growing tension between productivity and reliability. Generic programming aims at relieving this tension. The vision of this project is to develop a unifying theory of generic programming that will inform the design of future programming languages. Our goal is to produce a body of work that is in the same vein as the seminal work on Unifying Theories of Programming by Hoare and He: we consider the outcome of this project to be a unified foundation for generic programming that brings together the advantages of previous work into a coherent whole. From the perspective of increasing programmer productivity, the importance of understanding and applying generic programming has never been so critical. Software engineers are constantly faced with the challenge of adapting to changing specifications and designs, while ensuring that the ensuing refactoring maintains the correctness of the algorithms they have crafted. Our approach to solving this problem - generic programming - exploits the inherent structure that exists in data, where this structure can be used to automatically produce efficient and flexible algorithms that can be adapted to suit different needs. Furthermore, generic programs ensure that the structure of the data itself plays a central role in maintaining the correctness of these algorithms. The functional programming language Haskell offers rudimentary support for generic programming in the form of the deriving mechanism. Instead of manually coding, for example, equality for a datatype, the Haskell programmer attaches a simple hint to the datatype declaration which instructs the compiler to auto-generate equality and inequality for the datatype. Simple, convenient and robust. If the datatype is changed at a later point in time, equality and inequality are modified accordingly behind the scenes, supporting software evolution and easing software maintenance. Haskell's support for generic programming is only partial, as the deriving mechanism is limited to a few predefined classes. In particular, one cannot define new derivable classes. This is exactly what generic programming supports. Informally, a derivable or generic function is defined by induction on the structure of types. The generic programmer provides code for a few type constructs, the rest is taken care of automatically. The generic program can then be instantiated many times at different types. The last two decades have witnessed a number of approaches to generic programming differing in convenience, expressiveness and efficiency. We can roughly distinguish two main approaches: algebraic and type-theoretic ones. Both come with their various strengths and weaknesses. This project seeks to generalise and unify the two approaches, combining their individual strengths. It will do so using methods from a branch of mathematics called Category Theory. Furthermore, the project will explore novel approaches for the specification of generic programs, provide the infrastructure for reasoning about generic programs, and demonstrate that GP has far-reaching and important applications in practice.
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.ox.ac.uk