Jason Z. S. Hu ; Brigitte Pientka - A Categorical Normalization Proof for the Modal Lambda-Calculus

entics:10360 - Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1 - Proceedings of MFPS XXXVIII - https://doi.org/10.46298/entics.10360
A Categorical Normalization Proof for the Modal Lambda-CalculusArticle

Authors: Jason Z. S. Hu ORCID; Brigitte Pientka ORCID

    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.


    Volume: Volume 1 - Proceedings of MFPS XXXVIII
    Published on: February 22, 2023
    Accepted on: November 25, 2022
    Submitted on: November 23, 2022
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,D.3.1,F.4.1

    Consultation statistics

    This page has been seen 266 times.
    This article's PDF has been downloaded 201 times.