Categorical reconstruction of a reduction free normalization proof

DOI10.1007/3-540-60164-3_27MaRDI QIDQ5057474zbMATH OpenOpenAlexFDO

Authors Thorsten Altenkirch, Martin Hofmann, Thomas Streicher

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

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

Cites work

• Constructivism in mathematics. An introduction. Volume II
• scientific article; zbMATH DE number 2185660 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1555179 (Why is no real title available?)
• scientific article; zbMATH DE number 3260754 (Why is no real title available?)
• Intuitionistic model constructions and normalization proofs
• Kripke-style models for typed lambda calculus

Cited in

(21)

• Term rewriting for normalization by evaluation.
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Normalization by evaluation and algebraic effects
• Everybody's got to be somewhere
• 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
• POPLMark reloaded: mechanizing proofs by logical relations
• Semantic analysis of normalisation by evaluation for typed lambda calculus
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
• Normalization by evaluation for modal dependent type theory
• Big step normalisation for type theory
• Normalization for multimodal type theory
• Normalization by evaluation for the lambek calculus
• A categorical normalization proof for the modal lambda-calculus
• Normalization for multimodal type theory
• Syntactically and semantically regular languages of -terms coincide through logical relations
• A sound and complete substitution algorithm for multimode type theory
• Displayed type theory and semi-simplicial types
• Toward a geometry for syntax
• Deductive systems and coherence for skew prounital closed categories
• Formal \textsc{p}-category theory and normalization by evaluation in Rocq

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

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