A categorical normalization proof for the modal lambda-calculus

DOI10.46298/ENTICS.10360MaRDI QIDQ6831510zbMATH OpenFDO

Authors Jason Z. S. Hu, Brigitte Pientka

Publication date 2 April 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/ENTICS.10360

zbMATH Keywords

normalization by evaluationpresheaf modelmodal \(\lambda\)-calculuscontextual types

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites work

• scientific article; zbMATH DE number 1223735 (Why is no real title available?)
• scientific article; zbMATH DE number 699435 (Why is no real title available?)
• scientific article; zbMATH DE number 1848312 (Why is no real title available?)
• scientific article; zbMATH DE number 1405618 (Why is no real title available?)
• scientific article; zbMATH DE number 7297837 (Why is no real title available?)
• scientific article; zbMATH DE number 970633 (Why is no real title available?)
• A judgmental reconstruction of modal logic
• A modal analysis of staged computation
• A type theory for defining logics and proofs
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Categorical reconstruction of a reduction free normalization proof
• Contextual modal type theory
• Foundations of software science and computation structures. 21st international conference, FOSSACS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14--20, 2018. Proceedings
• Internal universes in models of homotopy type theory
• Modal dependent type theory and dependent right adjoints
• Multimodal dependent type theory
• On an intuitionistic modal logic
• Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi

This page was built for publication: A categorical normalization proof for the modal lambda-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6831510)