A Categorical Normalization Proof for the Modal Lambda-Calculus

TL;DR

This paper introduces a normalization by evaluation algorithm for a simply typed modal lambda-calculus, providing a logical foundation for multi-staged meta-programming and connecting modal semantics with context stack substitutions.

Contribution

It presents a sound and complete NbE algorithm for the modal lambda-calculus, integrating Kripke-style substitutions with context stacks and enabling a formal treatment of open code in meta-programming.

Findings

NbE algorithm is sound and complete for the calculus

Kripke-style substitutions unify modal transformations and assumptions

Framework supports representing open code in meta-programming

Abstract

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.