The correspondence between cut-elimination and normalization
From MaRDI portal
Publication:4052084
DOI10.1016/0003-4843(74)90010-2zbMath0298.02023OpenAlexW4206283588MaRDI QIDQ4052084
No author found.
Publication date: 1974
Published in: Annals of Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0003-4843(74)90010-2
Related Items (43)
A connection between cut elimination and normalization ⋮ A note on the proof theory of the \(\lambda \Pi\)-calculus ⋮ Algebraic proofs of cut elimination ⋮ Hypersequents, logical consequence and intermediate logics for concurrency ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications ⋮ Closed categories and the theory of proofs ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Three faces of natural deduction ⋮ A new reduction sequence for arithmetic ⋮ A coherence theorem for canonical morphisms in Cartesian closed categories ⋮ Growth of length of sequential derivation transformed into natural one ⋮ A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION ⋮ Normalization of N-graphs via sub-N-graphs ⋮ On the intuitionistic force of classical search (Extended abstract) ⋮ Prior's tonk, notions of logic, and levels of inconsistency: vindicating the pluralistic unity of science in the light of categorical logical positivism ⋮ Learning Lambek Grammars from Proof Frames ⋮ Yet another bijection between sequent calculus and natural deduction ⋮ Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi ⋮ On the form of witness terms ⋮ Variations on a theme of Curry ⋮ 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 ⋮ A study of Kripke-type models for some modal logics by Gentzen's sequential method ⋮ Prawitz, Proofs, and Meaning ⋮ Cut Elimination, Substitution and Normalisation ⋮ Theory of proofs (arithmetic and analysis) ⋮ Choice sequences and reduction processes ⋮ 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 ⋮ On the intuitionistic force of classical search ⋮ Maximum segments as natural deduction images of some cuts ⋮ CONSTRUCTIVE CLASSICAL LOGIC AS CPS-CALCULUS ⋮ Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation ⋮ A cut-elimination proof in intuitionistic predicate logic ⋮ Structural cut elimination. I: Intuitionistic and classical logic ⋮ On sequence-conclusion natural deduction systems ⋮ Full intuitionistic linear logic
This page was built for publication: The correspondence between cut-elimination and normalization
