| EPSRC Reference: |
EP/N02706X/2 |
| Title: |
Semantic Foundations for Interactive Programs |
| Principal Investigator: |
Krishnaswami, Dr N |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
First Grant - Revised 2009 |
| Starts: |
01 November 2016 |
Ends: |
28 February 2019 |
Value (£): |
96,282
|
| 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 |
When we first explain how computer programs work to beginners, we tend to explain them as a way of telling a computer how to implement an input-output relation: matrix libraries take a system of linear equations and compute a solution; compilers take a source text as input, and produces an object file as output; and web browsers read an HTML file as input, and then renders it to a screen as output. However, the programs we actually use tend to be interactive. Instead of solving a system of equations once, we might put it into a spreadsheet and incrementally modify the parameters to explore the solution space. Instead of giving a program once to a compiler, we develop within an IDE, with our work flow interleaving the process of writing code and finding and repairing errors in the program. A web browser does not merely display an HTML document, but can programmatically update the page in response to user and server events.
However, implementing interactive programs is generally much more complicated than implementing one-shot input-output behaviour. Programmers do not get the input to their program all at once, but instead they get it piece-by-piece incrementally. Furthermore, the output also has to be produced incrementally, so that the user of a piece of software can observe and react to the output produced so far. As a result, ensuring that the program keeps track of the user inputs and maintains a consistent view of what the user wants is quite difficult. Furthermore, the interactive behaviour of the program also makes it is harder to say what is and is not correct behaviour for the program, so even telling if a program is correct or incorrect can become very difficult.
The purpose of this project is to develop new programming languages that make writing interactive programs easier, in two ways. First, we will develop mathematical techniques to make it easier to formally state what a program should do, and to check that programs are satisfy this specification, and second, we seek to develop implementation techniques that ensure that interactive programs can run efficiently and respond in a timely fashion to user inputs.
|
|
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.cam.ac.uk |