Linear logic
From MaRDI portal
DOI10.1016/0304-3975(87)90045-4zbMATH Open0625.03037DBLPjournals/tcs/Girard87OpenAlexW2911865844WikidataQ28470256 ScholiaQ28470256MaRDI QIDQ579249FDOQ579249
Authors: Jean-Yves Girard 
Publication date: 1987
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(87)90045-4
Recommendations
proof theorylinear logiccut eliminationdomainsparallel processingsequent calculuspons asinorumnormalization procedureconstructive logicscontraction- free ruleslinear negationmechanical synthesis of programs from proofsmodality ``of courseproof-nets
General topics in the theory of software (68N01) Cut-elimination and normal-form theorems (03F05) Logic in computer science (03B70)
Cites Work
Cited In (only showing first 100 items - show all)
- Modeling linear logic with implicit functions
- Self-referentiality of Brouwer-Heyting-Kolmogorov semantics
- What is relevance logic?
- A logical framework combining model and proof theory
- Contraction, infinitary quantifiers, and omega paradoxes
- Coherent phase spaces. Semiclassical semantics
- Functional Interpretations of Intuitionistic Linear Logic
- Chu spaces from the representational viewpoint
- When are Two Algorithms the Same?
- Natural 3-valued logics—characterization and proof theory
- The conservation theorem for differential nets
- Figures of dialogue: a view from ludics
- A relational semantics for parallelism and non-determinism in a functional setting
- Light linear logics with controlled weakening: expressibility, confluent strong normalization
- Visible acyclic differential nets. I: Semantics
- Petri nets and bisimulation
- The Scott model of linear logic is the extensional collapse of its relational model
- A game semantics for linear logic
- On the expressiveness of interaction
- Rational mechanics and natural mathematics
- Timed Petri nets and temporal linear logic
- A computational interpretation of conceptivism
- Linearizing intuitionistic implication
- On phase semantics and denotational semantics: The exponentials
- Linear logic as a logic of computations
- A categorical reduction system for linear logic
- Linear Läuchli semantics
- Glueing and orthogonality for models of linear logic
- Many concepts and two logics of algorithmic reduction
- Interpreting a finitary pi-calculus in differential interaction nets
- On abstract resource semantics and computability logic
- The mix rule
- Propositions as sessions
- Focussing and proof construction
- Games and full abstraction for FPC.
- Polarized games
- Game-theoretic analysis of call-by-value computation
- Combining classical logic, paraconsistency and relevance
- The complexity of Horn fragments of linear logic
- Hypersequents, logical consequence and intermediate logics for concurrency
- Idempotent residuated structures: Some category equivalences and their applications
- Phase semantics for light linear logic
- Categorial graphs
- From multiple sequent for additive linear logic to decision procedures for free lattices
- Thick Subtrees, Games and Experiments
- Recovering quantum logic within an extended classical framework
- Generalized approximations of \(( \in ,\in \vee q) \)-fuzzy ideals in quantales
- Non-commutative logical algebras and algebraic quantales
- A new constructive logic: classic logic
- The displacement calculus
- On derivations of quantales
- A mathematical theory of resources
- Nuclei and conuclei on residuated lattices
- Characterization of projective quantales
- Relating toy models of quantum computation: comprehension, complementarity and dagger mix autonomous categories
- A correspondence between maximal abelian sub-algebras and linear logic fragments
- Algebraic logic for classical conjunction and disjunction
- Interface synthesis and protocol conversion
- Generalized approximation of substructures in quantales by soft relations
- Categorical proof theory of classical propositional calculus
- Combining behavioural types with security analysis
- Topological representation and quantic separation axioms of semi-quantales
- Alias burying: Unique variables without destructive reads
- A stable programming language
- From truth to computability. I.
- The quantic conuclei on quantales
- Cycling in proofs and feasibility
- A modal walk through space
- Computation with classical sequents
- Modal companions of intermediate propositional logics
- Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
- The parametric continuation monad
- Transcendental syntax I: deterministic case
- Interaction graphs: graphings
- Non-uniform hypercoherences
- A category equivalence for odd Sugihara monoids and its applications
- Quantum computation: from a programmer's perspective
- Static typing for a substructural lambda calculus
- Proof systems and transformation games
- Probabilistic coherence spaces as a model of higher-order probabilistic computation
- An abstract approach to consequence relations
- The taming of recurrences in computability logic through cirquent calculus. I
- Nonsymmetric \(^{\ast}\)-autonomous categories
- Focusing and polarization in linear, intuitionistic, and classical logics
- Games and full completeness for multiplicative linear logic
- Coalgebras, Chu spaces, and representations of physical systems
- Big toy models. Representing physical systems as Chu spaces
- Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions
- A representation theorem for quantales
- On the unity of logic
- A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic
- Multiplicative conjunction and an algebraic meaning of contraction and weakening
- Light Linear Logic with Controlled Weakening
- Natural deduction and coherence for weakly distributive categories
- Common knowledge logic in a higher order proof assistant
- Title not available (Why is that?)
- Cut elimination and strong separation for substructural logics: an algebraic approach
- Displacement logic for anaphora
- Subtyping for session types in the pi calculus
- Unary resolution: characterizing \textsc{Ptime}
This page was built for publication: Linear logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q579249)
