Pages that link to "Item:Q4052084"

The following pages link to The correspondence between cut-elimination and normalization (Q4052084):

Displaying 43 items.

• Prior's tonk, notions of logic, and levels of inconsistency: vindicating the pluralistic unity of science in the light of categorical logical positivism (Q516400) (← links)
• Yet another bijection between sequent calculus and natural deduction (Q530853) (← links)
• The \(\lambda \)-calculus and the unity of structural proof theory (Q733755) (← links)
• A connection between cut elimination and normalization (Q818516) (← links)
• On the form of witness terms (Q982183) (← links)
• Normal derivations and sequent derivations (Q1029828) (← links)
• On sequence-conclusion natural deduction systems (Q1062053) (← links)
• Closed categories and the theory of proofs (Q1147133) (← links)
• A new reduction sequence for arithmetic (Q1167719) (← links)
• A coherence theorem for canonical morphisms in Cartesian closed categories (Q1168319) (← links)
• Growth of length of sequential derivation transformed into natural one (Q1168320) (← links)
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi (Q1208732) (← links)
• A study of Kripke-type models for some modal logics by Gentzen's sequential method (Q1257012) (← links)
• Theory of proofs (arithmetic and analysis) (Q1260035) (← links)
• Permutability of proofs in intuitionistic sequent calculi (Q1275625) (← links)
• Termination of permutative conversions in intuitionistic Gentzen calculi (Q1275632) (← links)
• A cut-elimination proof in intuitionistic predicate logic (Q1304543) (← links)
• Full intuitionistic linear logic (Q1314646) (← links)
• Algebraic proofs of cut elimination (Q1349247) (← links)
• Hypersequents, logical consequence and intermediate logics for concurrency (Q1354077) (← links)
• On the intuitionistic force of classical search (Q1575923) (← links)
• Normalization of N-graphs via sub-N-graphs (Q1744401) (← links)
• Structural cut elimination. I: Intuitionistic and classical logic (Q1854335) (← links)
• A note on the proof theory of the \(\lambda \Pi\)-calculus (Q1891931) (← links)
• What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics (Q2037304) (← links)
• Maximum segments as natural deduction images of some cuts (Q2084573) (← links)
• Variations on a theme of Curry (Q2505136) (← links)
• Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications (Q2683029) (← links)
• A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION (Q3005996) (← links)
• Monadic Translation of Intuitionistic Sequent Calculus (Q3638248) (← links)
• Choice sequences and reduction processes (Q4189272) (← links)
• A resource aware semantics for a focused intuitionistic calculus (Q4559602) (← links)
• AN ANALYSIS OF THE RULES OF GENTZEN’S<b><i>NJ</i></b>AND<b><i>LJ</i></b> (Q4577998) (← links)
• Three faces of natural deduction (Q4610312) (← links)
• On the intuitionistic force of classical search (Extended abstract) (Q4645244) (← links)
• The normalization theorem for extended natural deduction (Q4985610) (← links)
• Prawitz, Proofs, and Meaning (Q5213604) (← links)
• Cut Elimination, Substitution and Normalisation (Q5213610) (← links)
• CONSTRUCTIVE CLASSICAL LOGIC AS CPS-CALCULUS (Q5249031) (← links)
• Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation (Q5251185) (← links)
• Learning Lambek Grammars from Proof Frames (Q5414961) (← links)
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction (Q5458374) (← links)
• The elimination of maximum cuts in linear logic and BCK logic (Q6161950) (← links)