A Semantic Proof that Reducibility Candidates entail Cut Elimination

DOI10.4230/LIPICS.RTA.2012.133zbMATH Open1437.03164OpenAlexW2247658575MaRDI QIDQ5111901FDOQ5111901

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)

Cited In (2)

• Title not available (Why is that?)
• Proof normalization modulo

   Recommendations

• Towards a semantic characterization of cut-elimination 👍 👎
• Typed Lambda Calculi and Applications 👍 👎
• Title not available (Why is that?) 👍 👎
• 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 👍 👎

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)