Normalization as a homomorphic image of cut-elimination

Cited In (25)

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