Linear logic
From MaRDI portal
Publication:579249
DOI10.1016/0304-3975(87)90045-4zbMath0625.03037DBLPjournals/tcs/Girard87OpenAlexW2911865844WikidataQ28470256 ScholiaQ28470256MaRDI QIDQ579249
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
domainscut eliminationsequent calculuslinear logicproof theoryparallel processingnormalization procedurepons asinorumconstructive logicscontraction- free ruleslinear negationmechanical synthesis of programs from proofsmodality ``of courseproof-nets
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (only showing first 100 items - show all)
Multiparty session types as coherence proofs ⋮ Theorem proving graph grammars with attributes and negative application conditions ⋮ On concurrent behaviors and focusing in linear logic ⋮ Cut elimination for the unified logic ⋮ Generating semigroups for complete atomistic ortholattices ⋮ Uniqueness logic ⋮ Structure of proofs and the complexity of cut elimination ⋮ Linear and affine logics with temporal, spatial and epistemic operators ⋮ A verification framework for agent programming with declarative goals ⋮ Proof checking and logic programming ⋮ A proof theoretic view of spatial and temporal dependencies in biochemical systems ⋮ Coherence in SMCCs and equivalences on derivations in IMML with unit ⋮ The intuitionistic fragment of computability logic at the propositional level ⋮ Strong planning under uncertainty in domains with numerous but identical elements (a generic approach) ⋮ The differential \(\lambda \mu\)-calculus ⋮ On the scope of some formulas defining additive connectives in fuzzy logics ⋮ Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols ⋮ On the value of variables ⋮ On subexponentials, focusing and modalities in concurrent systems ⋮ Differential logical relations. II: Increments and derivatives ⋮ Coalgebraic completeness-via-canonicity for distributive substructural logics ⋮ Characterising spectra of equivalences for event structures, logically ⋮ Non-normal modal logics and conditional logics: semantic analysis and proof theory ⋮ Language models for some extensions of the Lambek calculus ⋮ Lattice-theoretic models of conjectures, hypotheses and consequences ⋮ Editorial introduction: substructural logics and metainferences ⋮ Dialectica principles via Gödel doctrines ⋮ On involutive nonassociative Lambek calculus ⋮ Parsing/theorem-proving for logical grammar \textit{CatLog3} ⋮ The laws of thought and the laws of truth as two sides of one coin ⋮ The displacement calculus ⋮ Infinitary action logic with multiplexing ⋮ On the semantics of parsing actions ⋮ Modal MTL-algebras ⋮ A framework for linear authorization logics ⋮ Sufficient conditions for cut elimination with complexity analysis ⋮ 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000 ⋮ The graphical Krivine machine ⋮ Type logics and pregroups ⋮ Parsing pregroup grammars and Lambek calculus using partial composition ⋮ Free ordered algebraic structures towards proof theory ⋮ Conditionals and consequences ⋮ Maximality and totality of stable functions in the category of stable bifinite domains ⋮ System BV is NP-complete ⋮ Analytic functors between presheaf categories over groupoids ⋮ Harmony in multiple-conclusion natural-deduction ⋮ Interface synthesis and protocol conversion ⋮ Classical \(F_{\omega}\), orthogonality and symmetric candidates ⋮ Call-by-name reduction and cut-elimination in classical logic ⋮ On the unity of duality ⋮ Normal proofs, cut free derivations and structural rules ⋮ A stable programming language ⋮ Dynamic non-commutative logic ⋮ Triangular norm based predicate fuzzy logics ⋮ Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions ⋮ Coherence for star-autonomous categories ⋮ The three dimensions of proofs ⋮ From truth to computability. I. ⋮ Geometrical semantics for linear logic (multiplicative fragment) ⋮ On structuring proof search for first order linear logic ⋮ Orthomodular lattices and quantales ⋮ Introduction: Inferences and proofs ⋮ On paradoxes in normal form ⋮ Computing with Semirings and Weak Rig Groupoids ⋮ Call-By-Push-Value from a Linear Logic Point of View ⋮ Classical By-Need ⋮ Game Semantics for Access Control ⋮ Contraction-free Proofs and Finitary Games for Linear Logic ⋮ Logical Semantics for Stability ⋮ Abstracting models of strong normalization for classical calculi ⋮ The decidability of the intensional fragment of classical linear logic ⋮ When-and how-can a cellular automaton be rewritten as a lattice gas? ⋮ Verification of spatial and temporal modalities in biochemical systems ⋮ Game Semantics for Bounded Polymorphism ⋮ Meta-entanglement ⋮ Generalized approximation of substructures in quantales by soft relations ⋮ Logical vs. behavioural specifications ⋮ Some studies in the approximation of \((\in_\gamma, \in_\gamma \vee q_\delta)\)-fuzzy substructures in quantales ⋮ A game-semantic model of computation ⋮ Supercover semantics for deontic action logic ⋮ Non decomposable connectives of linear logic ⋮ The finite model property for BCI and related systems ⋮ Bounded contraction and Gentzen-style formulation of Łukasiewicz logics ⋮ On injective constructions of \(S\)-semigroups ⋮ Weak linearization of the lambda calculus ⋮ A proof theory for model checking ⋮ Proof diagrams for multiplicative linear logic: syntax and semantics ⋮ Syntax vs. semantics: A polarized approach ⋮ An interpretation of CCS into ludics ⋮ A concrete categorical semantics of lambda-\(\mathcal{S}\) ⋮ Term-generic logic ⋮ Genericity and the \(\pi\)-calculus ⋮ Subtyping for session types in the pi calculus ⋮ Order-enriched categorical models of the classical sequent calculus ⋮ Contrary-to-duty reasoning: a categorical approach ⋮ A structural approach to reversible computation ⋮ On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy ⋮ An abstract approach to stratification in linear logic ⋮ Quantitative classical realizability ⋮ Models and emerging trends of concurrent constraint programming
Cites Work
This page was built for publication: Linear logic
