A Core Calculus for Documents

Passive documents and active programs now widely comingle. Document languages include Turing-complete programming elements, and programming languages include sophisticated document notations. However, there are no formal foundations that model these languages. This matters because the interaction between document and program is complicated and can be error-prone. In this paper we describe several of these problems, then taxonomize these document languages, and model them as levels of a document calculus. We employ the calculus as a foundation for implementing complex runtime features such as reactivity, as well as for proving a few useful theorems regarding the boundary of content and computation. We intend for the document calculus to provide a theoretical basis for new document languages, and to enable designers to clean up the unsavory corners of existing ones.