A Semantic Proof that Reducibility Candidates entail Cut Elimination

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

Authors: Denis Cousineau, Olivier Hermant 

Publication date: 27 May 2020

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

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

zbMATH Keywords

cut eliminationreducibility candidates(pre-)Heyting algebras

Mathematics Subject Classification ID

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

Cited In (7)

• On completeness of reducibility candidates as a semantics of strong normalization
• Title not available (Why is that?)
• 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)