A Semantic Proof that Reducibility Candidates entail Cut Elimination

DOI10.4230/LIPIcs.RTA.2012.133zbMath1437.03164OpenAlexW2247658575MaRDI QIDQ5111901

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)

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