论文标题
模态lambda-calculus的分类标准化证明
A Categorical Normalization Proof for the Modal Lambda-Calculus
论文作者
论文摘要
由于Pfenning，Wong和Davies，我们研究了一个简单键入的模态$λ$ -calculus，$λ^{\ to \ square} $，在那里我们针对上下文堆栈定义了一个良好的术语，该列表以一种语法方式捕获可能的世界语义。它为多级元编程提供了逻辑基础。我们在本文中的主要贡献是通过评估（NBE）算法的归一化，以$λ^{\ to \ square} $进行，我们证明了声音并完成。 NBE算法是简单键入$λ$ -Calculus标准的Presheaf模型的中等扩展。但是，模型构建和NBE算法的核心是在上下文堆栈上观察到Kripke式替换的观察，这些替代汇集了两个先前独立的概念，即在上下文堆栈上的结构模态转换以及单个假设的替代。此外，Kripke风格的替换使我们能够为上下文类型提供公式，该公式可以在元编程设置中代表打开代码。我们的作品为通过Pfenning，Wong和Davies扩大逻辑基础的基础奠定了基础，以建立一个实用的，依赖的元编程基础。
We investigate a simply typed modal $λ$-calculus, $λ^{\to\square}$, due to Pfenning, Wong and Davies, where we define a well-typed term with respect to a context stack that captures the possible world semantics in a syntactic way. It provides logical foundation for multi-staged meta-programming. Our main contribution in this paper is a normalization by evaluation (NbE) algorithm for $λ^{\to\square}$ which we prove sound and complete. The NbE algorithm is a moderate extension to the standard presheaf model of simply typed $λ$-calculus. However, central to the model construction and the NbE algorithm is the observation of Kripke-style substitutions on context stacks which brings together two previously separate concepts, structural modal transformations on context stacks and substitutions for individual assumptions. Moreover, Kripke-style substitutions allow us to give a formulation for contextual types, which can represent open code in a meta-programming setting. Our work lays the foundation for extending the logical foundation by Pfenning, Wong, and Davies towards building a practical, dependently typed foundation for meta-programming.
