A Semantic Proof that Reducibility Candidates entail Cut Elimination

DOI10.4230/LIPICS.RTA.2012.133MaRDI QIDQ5111901zbMATH OpenOpenAlexFDO

Authors Denis Cousineau, Olivier Hermant

Publication date 27 May 2020

Full work available at URL https://hal-mines-paristech.archives-ouvertes.fr/hal-00743284

zbMATH Keywords

cut eliminationreducibility candidates(pre-)Heyting algebras

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Recommendations

• Towards a semantic characterization of cut-elimination
• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 6680140
• A cut-elimination proof in intuitionistic predicate logic
• Cut-elimination and proof schemata
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Cut Elimination in the Presence of Axioms
• Cut elimination for entailment relations
• Cut Elimination in ε‐Calculi

Cited in

(7)

• On completeness of reducibility candidates as a semantics of strong normalization
• scientific article; zbMATH DE number 6680140 (Why is no real title available?)
• Union of Reducibility Candidates for Orthogonal Constructor Rewriting
• Semantic A-translations and super-consistency entail classical cut elimination
• Towards a semantic characterization of cut-elimination
• On the Values of Reducibility Candidates
• Proof normalization modulo

This page was built for publication: A Semantic Proof that Reducibility Candidates entail Cut Elimination

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