Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions

DOI10.2178/jsl/1230396755zbMath1168.03041OpenAlexW2049453322MaRDI QIDQ3617369

Paweł Urzyczyn, Morten Heine B. Sørensen

Publication date: 23 March 2009

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2178/jsl/1230396755

zbMATH Keywords

strong cut-elimination

Mathematics Subject Classification ID

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

Cites Work

• Strong normalization proofs by CPS-translations
• Lectures on the Curry-Howard isomorphism
• Perpetual reductions in \(\lambda\)-calculus
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Strong normalization from weak normalization by translation into the lambda-I-calculus
• Perpetuality in a named lambda calculus with explicit substitutions
• Cut rules and explicit substitutions
• Explicit substitutions
• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
• Weak normalization implies strong normalization in a class of non-dependent pure type systems

This page was built for publication: Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions