We investigate a simply typed modal $\lambda$-calculus, $\lambda^{\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 $\lambda^{\to\square}$ which we prove sound and complete. The NbE algorithm is a moderate extension to the standard presheaf model of simply typed $\lambda$-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.

翻译：我们研究了一种由Pfenning、Wong和Davies提出的简单类型模态λ-演算λ^{→□}。在该演算中，我们基于上下文栈定义了良类型项，以语法形式捕捉可能世界语义。这为多阶段元编程提供了逻辑基础。本文的主要贡献在于为λ^{→□}提出了一种规范化求值（NbE）算法，并证明了其可靠性与完备性。该NbE算法是对简单类型λ-演算标准预层模型的适度扩展。然而，模型构造与NbE算法的核心在于对上下文栈上Kripke风格替换的观察——这融合了此前两个独立概念：上下文栈上的结构模态变换与个体假设替换。此外，Kripke风格替换使我们能够对上下文类型进行形式化描述，从而在元编程设定中表示开放代码。我们的工作为扩展Pfenning、Wong和Davies的逻辑基础，构建基于依赖类型的实用元编程基石奠定了基础。