Linear logic

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

• scientific article; zbMATH DE number 4023271
• The semantics and proof theory of linear logic
• Publication:4896506
• Free-cut elimination in linear logic and an application to a feasible arithmetic
• scientific article; zbMATH DE number 1489627

zbMATH Keywords

proof theorylinear logiccut eliminationdomainsparallel processingsequent calculuspons asinorumnormalization procedureconstructive logicscontraction- free ruleslinear negationmechanical synthesis of programs from proofsmodality ``of courseproof-nets

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Cut-elimination and normal-form theorems (03F05) Logic in computer science (03B70)

Cites Work

• The system \({\mathcal F}\) of variable types, fifteen years later
• Normal functors, power series and \(\lambda\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Execution time of λ-terms via denotational semantics and intersection types
• The finite model property for various fragments of intuitionistic linear logic
• Quantales, observational logic and process semantics
• Structure of left-continuous triangular norms with strong induced negations (II) Rotation-annihilation construction
• Pretopologies and completeness proofs
• N.A. Vasil'ev's logical ideas and the categorical semantics of many-valued logic
• Current trends in substructural logics
• Bunched sequential information
• The eco-cognitive model of abduction. II. Irrelevance and implausibility exculpated
• Logical consequence and the paradoxes
• A micrological study of negation
• Naive \textit{modus ponens}
• Temporal BI: proof system, semantics and translations
• Parsing/theorem-proving for logical grammar \textit{CatLog3}
• Disjunctive systems and L-Domains
• A semantic account of strong normalization in linear logic
• A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization
• Computation by interaction for space-bounded functional programming
• Ternary relations and relevant semantics
• Resource modalities in tensor logic
• Weakly distributive categories
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• Specifying properties of concurrent computations in CLF
• A semantic measure of the execution time in linear logic
• A calculus and logic of resources and processes
• Free \(Q\)-algebras.
• Category theory, logic and formal linguistics: some connections, old and new
• Formal ontologies and coherent spaces
• Dynamic spaces in concurrent constraint programming
• Relational semantics for full linear logic
• The semantics and proof theory of linear logic
• Optimal reductions in interaction systems
• The largest cartesian closed category of stable domains
• Computational interpretations of linear logic
• Interaction graphs: multiplicatives
• Domain theory in logical form
• Decision problems for propositional linear logic
• Intuitionistic differential nets and lambda-calculus
• Differential interaction nets
• Quine and Slater on paraconsistency and deviance
• Interaction graphs: additives
• Contextual deduction theorems
• Uniformity and the Taylor expansion of ordinary lambda-terms
• Representation theorems for \(Q\)-algebras
• A logic of separating modalities
• Monoidal t-norm based logic: Towards a logic for left-continuous t-norms
• Automata theory based on complete residuated lattice-valued logic: Turing machines
• Strong normalization property for second order linear logic
• Introduction to computability logic
• A non-deterministic view on non-classical negations
• From IF to BI. A tale of dependence and separation
• Stable neighbourhoods
• Bounded linear logic: A modular approach to polynomial-time computability
• Cut and pay
• Pumping lemma in automata theory based on complete residuated lattice-valued logic: a note
• Resources, concurrency, and local reasoning
• Constructing \(Q\)-algebras from \(Q\)-modules
• Light linear logic
• A note on Trillas' CHC models
• Automata theory based on complete residuated lattice-valued logic: Reduction and minimization
• Automata theory based on complete residuated lattice-valued logic: Pushdown automata
• On the algebraic structure of declarative programming languages
• Automata theory based on complete residuated lattice-valued logic: a categorical approach
• Linear logic and elementary time
• Some points in formal topology.
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Build your own clarithmetic. I: Setup and completeness
• Pragmatic and dialogic interpretations of bi-intuitionism. I
• An internal language for autonomous categories
• Gödel's system \(\mathcal T\) revisited
• Soft linear logic and polynomial time
• Quantale algebras as lattice-valued quantales
• Dynamic non-commutative logic
• Algebraic and categorical aspects of quantales
• Böhm's theorem for resource lambda calculus through Taylor expansion
• A characterization theorem on the rotation construction for triangular norms
• Completeness results for linear logic on Petri nets
• Linear and affine logics with temporal, spatial and epistemic operators
• The intuitionistic fragment of computability logic at the propositional level
• The differential lambda-calculus
• The decidability of the intensional fragment of classical linear logic
• A structural approach to reversible computation
• On the logic of expansion in natural language
• An epistemic separation logic
• A modal BI logic for dynamic resource properties
• Triangular norm based predicate fuzzy logics
• Models and emerging trends of concurrent constraint programming
• On quantum lambda calculi: a foundational perspective
• A verification framework for agent programming with declarative goals
• Kripke models for linear logic
• Soft linear logic and polynomial complexity classes
• Sufficient conditions for cut elimination with complexity analysis
• Processes and games
• Functions as processes
• On traced monoidal closed categories
• Enriching an Effect Calculus with Linear Types
• A model for syntactic control of interference
• Quantales and (noncommutative) linear logic
• Some reasons for generalising domain theory
• Assertion, Denial and Non-classical Theories

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)