A new deconstructive logic: linear logic

DOI10.2307/2275572zbMATH Open0895.03023OpenAlexW2164691248MaRDI QIDQ4372906FDOQ4372906

Authors: Vincent Danos, Jean-Baptiste Joinet, Harold Schellinx 

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

Recommendations

• On the non-confluence of cut-elimination
• scientific article; zbMATH DE number 742720
• scientific article; zbMATH DE number 1342291
• scientific article; zbMATH DE number 1722658
• From propositional to linear logic: An introduction. Decoration, simulation, normalization

zbMATH Keywords

normal formclassical logiccut-eliminationChurch-Rosser propertytranslations into linear logic

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (39)

• Proofs of strong normalisation for second order classical natural deduction
• Constructive classical logic as CPS-calculus
• Cut elimination for the unified logic
• Polarized and focalized linear and classical proofs
• On the form of witness terms
• A logical characterization of forward and backward chaining in the inverse method
• Polarized games
• Strong normalization property for second order linear logic
• Polarized proof-nets and \(\lambda \mu\)-calculus
• The additive multiboxes
• Linear logic and elementary time
• Call-by-name reduction and cut-elimination in classical logic
• Computational isomorphisms in classical logic
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Structure of proofs and the complexity of cut elimination
• Focusing Gentzen's LK proof system
• Proving termination of evaluation for system F with control operators
• Classical call-by-need and duality
• Title not available (Why is that?)
• Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
• Computation with classical sequents
• Proof Transformations and Structural Invariance
• Proofs, reasoning and the metamorphosis of logic
• A focused approach to combining logics
• Focalisation and Classical Realisability
• Focusing and polarization in linear, intuitionistic, and classical logics
• Title not available (Why is that?)
• Preface to the special volume
• Strong normalization for all-style \(\mathbf{LK}^\mathrm{tq}\)
• On the linear decoration of intuitionistic derivations
• On the unity of logic
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• Expansion trees with cut
• Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
• A Clausal Approach to Proof Analysis in Second-Order Logic
• On the unity of duality
• A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points
• Towards the animation of proofs -- testing proofs by examples
• Proof nets for classical logic

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4372906)