Semantic Foundations for Interactive Programs

当我们第一次向初学者解释计算机程序如何工作时，我们倾向于将它们解释为告诉计算机如何实现输入-输出关系的一种方式：矩阵库采用线性方程组并计算解；编译器将源文本作为输入，并产生一个目标文件作为输出；web浏览器读取HTML文件作为输入，然后将其作为输出呈现到屏幕上。然而，我们实际使用的程序往往是交互式的。我们可以将方程组放入电子表格中，并逐步修改参数以探索解空间，而不是一次性地求解方程组。我们不再将程序一次性交给编译器，而是在IDE中进行开发，我们的工作流程穿插着编写代码和查找和修复程序中的错误的过程。web浏览器不仅显示HTML文档，还可以通过编程方式更新页面以响应用户和服务器事件。然而，实现交互式程序通常比实现一次输入-输出行为要复杂得多。程序员不会一次得到程序的所有输入，而是增量地一点一点地得到输入。此外，输出还必须以增量的方式产生，以便软件的用户可以观察到目前为止产生的输出并对其作出反应。因此，确保程序跟踪用户输入并保持用户所需内容的一致视图是相当困难的。此外，程序的交互行为也使得很难说什么是程序的正确行为，什么不是程序的正确行为，因此甚至判断程序是否正确都变得非常困难。这个项目的目的是开发新的编程语言，以两种方式使编写交互式程序更容易。首先，我们将开发数学技术，使其更容易正式地说明程序应该做什么，并检查程序是否满足此规范，其次，我们将寻求开发实现技术，以确保交互式程序能够有效运行并及时响应用户输入。

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.