The core contribution of our paper is a formal model of document languages. This model extends System F with the concept of templates. We provide static and dynamic semantics for templates, and we also model various run-time extensions to the system such as reference labeling and reactivity.
~
CRICHTON, Will and KRISHNAMURTHI, Shriram, 2024. A Core Calculus for Documents: Or, Lambda: The Ultimate Document. Proceedings of the ACM on Programming Languages. 5 January 2024. Vol. 8, no. POPL, p. 23:667-23:694. doi 
and related artifacts zenodo , github pdf blog
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.