A new deconstructive logic: linear logic
From MaRDI portal
Publication:4372906
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
Related Items
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
