一句话：提出文档演算，将文档语言分层形式化，为混合文档与程序的语言提供形式基础并支持反应式等特性。
被动文档与主动程序日益交织：文档语言包含图灵完备的编程元素，编程语言也提供复杂文档记号，但缺乏形式基础来建模二者交互，导致微妙且易错的语义问题。本文先列举此类问题，随后对文档语言进行分类，并将其形式化为文档演算的不同层级。作者用该演算作为实现反应式等复杂特性的基础，并证明关于内容与计算边界的定理。其目标是为新文档语言提供理论基础，并帮助设计者清理现有语言中不优雅的角落。
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 can be subtle and error-prone. In this paper we describe several such problems, then taxonomize and formalize document languages as levels of a document calculus. We employ the calculus as a foundation for implementing complex features such as reactivity, as well as for proving theorems about the boundary of content and computation. We intend for the document calculus to provide a theoretical basis for new document languages, and to assist designers in cleaning up the unsavory corners of existing languages.
@article{paperbot2604,
title = {A Core Calculus for Documents: Or, Lambda: The Ultimate Document},
author = {Will Crichton and Shriram Krishnamurthi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632865}
}