Semantic Foundations for Interactive Programs

当我们第一次向初学者解释计算机程序如何工作时，我们倾向于将其解释为告诉计算机如何实现输入-输出关系的一种方式：矩阵库获取线性方程系统并计算解；编译器将源文本作为输入，并产生目标文件作为输出；网络浏览器将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.