Normalization as a homomorphic image of cut-elimination

Cited in

(27)

Normal derivations and sequent derivations
An interpretation of classical proofs
On sequence-conclusion natural deduction systems
A new reduction sequence for arithmetic
Permutability of proofs in intuitionistic sequent calculi
Termination of permutative conversions in intuitionistic Gentzen calculi
Full intuitionistic linear logic
What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
Maximum segments as natural deduction images of some cuts
Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment
A sequent calculus isomorphic to Gentzen's natural deduction
Monadic Translation of Intuitionistic Sequent Calculus
A resource aware semantics for a focused intuitionistic calculus
AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
Three faces of natural deduction
The normalization theorem for extended natural deduction
Cut elimination, substitution and normalisation
Constructive classical logic as CPS-calculus
Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
Yet another bijection between sequent calculus and natural deduction
Strong Normalisation of Cut-Elimination That Simulates β-Reduction
The elimination of maximum cuts in linear logic and BCK logic
Sequent images of normal derivations and natural deduction images of derivations without m-cuts
Gentzen-Mints-Zucker duality
The \(\lambda \)-calculus and the unity of structural proof theory
A connection between cut elimination and normalization
Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage

This page was built for publication: Normalization as a homomorphic image of cut-elimination

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