A new deconstructive logic: linear logic
From MaRDI portal
Recommendations
Cites work
- A general storage theorem for integers in call-by-name \(\lambda\)- calculus
- A new constructive logic: classic logic
- A symmetric lambda calculus for classical program extraction
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Classical logic, storage operators and second-order lambda-calculus
- Coherent models of proof nets
- Cut elimination for the unified logic
- scientific article; zbMATH DE number 46869 (Why is no real title available?)
- Linear logic
- On the Interpretation of Non-Finitist Proofs--Part I
- On the linear decoration of intuitionistic derivations
- On the unity of logic
- Proof strategies in linear logic
- Recursive programming with proofs
- Untersuchungen über das logische Schliessen. II
Cited in
(42)- Focusing and polarization in linear, intuitionistic, and classical logics
- Strong normalization property for second order linear logic
- Prolegomena of a logic of causality and dynamism
- On the linear decoration of intuitionistic derivations
- Computational isomorphisms in classical logic
- Linear logic and elementary time
- Polarized proof-nets and \(\lambda \mu\)-calculus
- The additive multiboxes
- Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
- Polarized games
- Proof nets for classical logic
- Cut elimination for the unified logic
- Structure of proofs and the complexity of cut elimination
- Call-by-name reduction and cut-elimination in classical logic
- On the unity of duality
- Classical call-by-need and duality
- Computation with classical sequents
- A Clausal Approach to Proof Analysis in Second-Order Logic
- Focalisation and Classical Realisability
- scientific article; zbMATH DE number 742720 (Why is no real title available?)
- Proofs of strong normalisation for second order classical natural deduction
- Strong normalization for all-style \(\mathbf{LK}^\mathrm{tq}\)
- Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
- Proving termination of evaluation for system F with control operators
- The true concurrency of Herbrand's theorem
- Expansion trees with cut
- Constructive classical logic as CPS-calculus
- Proofs, reasoning and the metamorphosis of logic
- Preface to the special volume
- Proof Transformations and Structural Invariance
- Strong Normalisation of Cut-Elimination That Simulates β-Reduction
- Polarized and focalized linear and classical proofs
- Towards the animation of proofs -- testing proofs by examples
- A focused approach to combining logics
- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points
- Focusing Gentzen's LK proof system
- On the unity of logic
- On the cut-elimination of the modal -calculus: linear logic to the rescue
- Gödel's absolute proofs and Girard's ludics: mutual insights
- A logical characterization of forward and backward chaining in the inverse method
- CERES: An analysis of Fürstenberg's proof of the infinity of primes
- On the form of witness terms
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)
