Categorical reconstruction of a reduction free normalization proof

DOI10.1007/3-540-60164-3_27zbMath1502.03019OpenAlexW1765415708MaRDI QIDQ5057474

Martin Hofmann, Thomas Streicher, Thorsten Altenkirch

Publication date: 16 December 2022

Published in: Category Theory and Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-60164-3_27

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (11)

Normalization by evaluation and algebraic effects ⋮ Semantic analysis of normalisation by evaluation for typed lambda calculus ⋮ Normalization by evaluation for modal dependent type theory ⋮ Term rewriting for normalization by evaluation. ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs ⋮ A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.

Cites Work

• Kripke-style models for typed lambda calculus
• Constructivism in mathematics. An introduction. Volume II
• Intuitionistic model constructions and normalization proofs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Categorical reconstruction of a reduction free normalization proof