A new deconstructive logic: linear logic

DOI10.2307/2275572zbMath0895.03023OpenAlexW2164691248MaRDI QIDQ4372906

Jean-Baptiste Joinet, Harold Schellinx, Vincent Danos

Publication date: 5 April 1998

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2275572

zbMATH Keywords

normal formcut-eliminationclassical logicChurch-Rosser propertytranslations into linear logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items (34)

Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus ⋮ Structure of proofs and the complexity of cut elimination ⋮ Polarized games ⋮ On the linear decoration of intuitionistic derivations ⋮ Unnamed Item ⋮ Computational isomorphisms in classical logic ⋮ Linear logic and elementary time ⋮ Computation with classical sequents ⋮ A focused approach to combining logics ⋮ A logical characterization of forward and backward chaining in the inverse method ⋮ Proof nets for classical logic ⋮ CERES: An analysis of Fürstenberg's proof of the infinity of primes ⋮ Classical Call-by-Need and Duality ⋮ Strong normalization for all-style LKtq ⋮ Proofs of strong normalisation for second order classical natural deduction ⋮ Towards Hilbert's 24th Problem: Combinatorial Proof Invariants ⋮ Preface to the special volume ⋮ Call-by-name reduction and cut-elimination in classical logic ⋮ On the unity of duality ⋮ Proof Transformations and Structural Invariance ⋮ Polarized and focalized linear and classical proofs ⋮ Unnamed Item ⋮ On the form of witness terms ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic ⋮ Towards the animation of proofs -- testing proofs by examples ⋮ Strong Normalisation of Cut-Elimination That Simulates β-Reduction ⋮ Focalisation and Classical Realisability ⋮ Expansion trees with cut ⋮ Focusing and polarization in linear, intuitionistic, and classical logics ⋮ Strong normalization property for second order linear logic ⋮ CONSTRUCTIVE CLASSICAL LOGIC AS CPS-CALCULUS ⋮ Proofs, Reasoning and the Metamorphosis of Logic ⋮ Polarized proof-nets and \(\lambda \mu\)-calculus ⋮ The additive multiboxes

Cites Work

• Unnamed Item
• Linear logic
• On the unity of logic
• Recursive programming with proofs
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Coherent models of proof nets
• Classical logic, storage operators and second-order lambda-calculus
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• Proof strategies in linear logic
• On the linear decoration of intuitionistic derivations
• Untersuchungen über das logische Schliessen. II
• A symmetric lambda calculus for classical program extraction
• Cut elimination for the unified logic
• A new constructive logic: classic logic
• On the Interpretation of Non-Finitist Proofs--Part I

This page was built for publication: A new deconstructive logic: linear logic