Normalization as a homomorphic image of cut-elimination

Cited in

(25)

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

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)