# EP/G033056/1 - Theory And Applications of Induction Recursion

Research Perspectives grant details from EPSRC portfolio

EPSRC Database

Source RCUK EPSRC Data

Research Perspectives grant details from EPSRC portfolio

Principal Investigator - Computer and Information Sciences, University of Strathclyde

Scheme

Standard Research

Research Areas

Programming Languages and Compilers

Related Grants

EP/G03298X/1

EP/G033374/1

Start Date

03/2009

End Date

08/2012

Value

£310,904

Similar Grants

Automatic generation of similar EPSRC grants

Similar Topics

Topic similar to the description of this grant

Grant Description

Summary and Description of the grant

Computers are good at adding billions of numbers in microseconds. Humans, on the other hand, are good at abstract thinking. This is exemplified by the development of philosophy, literature, science and mathematics. These observations have deep consequences for programming and the design of programming languages. The overarching concern of much research in computer science is to minimize the difference between how humans conceptualise programs and how those programs are implemented in a programming language. To achieve this, we do the same thing humans have been doing for 5000 years as we try to understand the world around us. That is, we construct mathematical models --- in this case, mathematical models of computation - and then reflect that understanding of computation within the design of programming languages. Thus, there is a symbiotic relationship between mathematics, programming, and the design of programming languages, and any attempt to sever this connection will diminish each component. Recursion is one of the most fundamental mathematical concepts in computation. Its importance lies in the ability it gives us to define computational agents in terms of themselves - these could be recursive programs, recursive data types, recursive algorithms or any of a myriad of otherstructures. The original treatments of recursion go back to the 1930s where the concept of computability was formalised via the theory ofgeneral recursive functions. It is virtually impossible to overestimate how recursion has contributed to our ability to computeand to understand the process of computation. Is it possible that there is anything fundamental left to say about recursion? We believe there is. Our central insight is this: when defining a function recursively, the inputs of the function are usually fixed in advance. But what if they are not? What if, as we build up the function recursively, we also build up its inputs inductively? The study of functions defined in this way is called induction recursion and this proposal aims to develop the theory and applications of induction recursion.Our central ambition is to turn induction recursion, which is currently known only to a relatively small number of researchers within type theory, into a mainstream technique within the programming language community. This will require both the theoretical development of induction recursion so as to give us more ways to understand it, but also case studies and examples to make it more accessible to programmers. Fortunately this is an excellent time to do this research! The categorical study of data types has advanced to the stage where the theoretical tools are now in place to tackle inductionrecursion. Perhaps even more fundamentally, dependently typed programming languages in the shape of Epigram and Agda have advancedto the stage where our ideas can be implemented in code and hence the benefits of induction recursion can be made directly available toprogrammers in a form they understand. We can supply them with code to play with! Indeed, we hope to go even further an explore the extent to which induction recursion can form the basis of a programming language. In summary, this proposal takes state of the art ideas in theoretical computer science and will aim to turn them directly into state of the art techniques within programming languages. Such combinations of theory and applications going hand in hand together is often the hall mark of good science!

EPSRC Grants On The Web Link

http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/G033056/1

Structured Data / Microdata

Grant Event Details:

Name: Theory And Applications of Induction Recursion - EP/G033056/1

Start Date: 2009-03-01T00:00:00+00:00

End Date: 2012-08-31T00:00:00+00:00

Organization: University of Strathclyde

Description: Computers are good at adding billions of numbers in microseconds. Humans, on the other hand, are good at abstract thinking. This is exemplified by the development of philosophy, literature, science and mathematics. These observations have deep consequences ...