Semantic Foundations for Interactive Programs

点击翻译按钮获取中文摘要

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.