Normalization as a homomorphic image of cut-elimination
From MaRDI portal
Publication:4156419
DOI10.1016/S0003-4843(77)80004-1zbMath0378.02017WikidataQ122966847 ScholiaQ122966847MaRDI QIDQ4156419
Publication date: 1977
Published in: Annals of Mathematical Logic (Search for Journal in Brave)
Related Items
A connection between cut elimination and normalization ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Three faces of natural deduction ⋮ A new reduction sequence for arithmetic ⋮ Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage ⋮ A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION ⋮ Yet another bijection between sequent calculus and natural deduction ⋮ Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment ⋮ What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics ⋮ The \(\lambda \)-calculus and the unity of structural proof theory ⋮ Strong Normalisation of Cut-Elimination That Simulates β-Reduction ⋮ Cut Elimination, Substitution and Normalisation ⋮ Monadic Translation of Intuitionistic Sequent Calculus ⋮ Permutability of proofs in intuitionistic sequent calculi ⋮ Termination of permutative conversions in intuitionistic Gentzen calculi ⋮ Normal derivations and sequent derivations ⋮ The normalization theorem for extended natural deduction ⋮ Maximum segments as natural deduction images of some cuts ⋮ CONSTRUCTIVE CLASSICAL LOGIC AS CPS-CALCULUS ⋮ An interpretation of classical proofs ⋮ Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation ⋮ On sequence-conclusion natural deduction systems ⋮ Full intuitionistic linear logic
This page was built for publication: Normalization as a homomorphic image of cut-elimination
