A Core Calculus for Documents (2024)
The paper introduces a core calculus for documents, formalizing document construction, transformation, and rendering operations based on combinators like doc, nest, line, group, and sep. It provides a denotational semantics grounded in an algebraic structure of documents and proves properties like confluence and normalization for the calculus.
Background
- This academic paper proposes a formal "core calculus" (a minimal mathematical model) for thinking about documents — not just static text files, but dynamic, structured, interactive documents like modern web pages or rich user interfaces.
- The authors argue that mainstream programming languages lack a clean theoretical foundation for documents, which mix layout, scripting, styling, and data. They aim to provide one, analogous to how the lambda calculus provides a foundation for computation.
- The work sits at the intersection of programming languages research, document engineering, and human-computer interaction. It extends prior work on "literate programming" (mixing code and prose) and "bidirectional transformations" (keeping data and its rendered display in sync).
- Why this matters: As software increasingly delivers experiences through documents (web apps, notebooks like Jupyter, interactive reports), having a rigorous calculus could influence how future document systems are designed, verified, and composed — making them more reliable and less ad-hoc.