文档核心演算（2024）
本文提出了一种用于文档建模的核心演算（core calculus），旨在为文档的结构、内容与操作提供形式化的理论基础。该演算统一了文档的树状结构与交互行为，支持类型安全的文档变换和查询。研究为编程语言中文档处理子系统的设计与验证奠定了形式语义基础。
背景速读
- 这篇论文提出了一种名为 λ-doc 的“文档核心演算”，属于编程语言理论（PL 理论）领域的研究。它试图从数学上精确回答一个根本问题：“文档到底是什么？”
- 过去几十年里，人们把网页（HTML）和文字处理文件（如 Word、LaTeX）都叫“文档”，但缺乏统一的形式化模型。这篇论文试图填补这个空缺。
- λ-doc 的核心思路是：将文档视为一个“求值后产生树状结构”的表达式，可以包含变量、函数应用、条件分支等编程语言才有的特性。这比传统 HTML 的静态嵌套更灵活。
- 这项研究对“声明式 UI 框架”（如 React 的 JSX、SwiftUI、Flutter）有直接意义——这些框架都允许在界面中嵌入逻辑，但底层缺少严格的理论支撑。λ-doc 试图为这类系统提供数学基础。
- 论文发表在 ACM 会议 ICFP 2024 上，该会议是编程语言领域最顶级的学术会议之一。作者来自多所大学和微软研究院。