Linear logic
From MaRDI portal
Publication:579249
DOI10.1016/0304-3975(87)90045-4zbMath0625.03037OpenAlexW2911865844WikidataQ28470256 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
Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) General topics in the theory of software (68N01)
Related Items
Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), From IF to BI. A tale of dependence and separation, Prime algebraicity, Behavioral interface description of an object-oriented language with futures and promises, Cut and pay, Pumping lemma in automata theory based on complete residuated lattice-valued logic: a note, A calculus and logic of resources and processes, The linear abstract machine, The semantics and proof theory of linear logic, Categorical proof theory of classical propositional calculus, Differential interaction nets, Remarks on classifications and adjunctions, Weak typed Böhm theorem on IMLL, BCK-combinators and linear \(\lambda\)-terms have types, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Resource operators for \(\lambda\)-calculus, Resources, concurrency, and local reasoning, Natural deduction and coherence for weakly distributive categories, Algebraic structures in categorial grammar, Fuzzy logics based on \([0,1)\)-continuous uninorms, Combining behavioural types with security analysis, Interaction graphs: additives, Proof nets and the call-by-value \(\lambda\)-calculus, Subexponential concurrent constraint programming, Filters on some classes of quantum B-algebras, A typed calculus based on a fragment of linear logic, Axioms and models of linear logic, Rigid E-unification: NP-completeness and applications to equational matings, On formalisms, Domain theory in logical form, Inheritance as implicit coercion, Parametric \(\lambda \)-theories, The undecidability of \(k\)-provability, A characterization of nuclei in orthomodular and quantic lattices, Language in action, A bridge between constructive logic and computer programming, Relevant logic programming, Implementing the `Fool's model' of combinatory logic, Quantaloidal nuclei, the syntactic congruence and tree automata, Binary logic is rich enough, Stable neighbourhoods, Quantitative domains and infinitary algebras, Soft linear set theory, Uniformity and the Taylor expansion of ordinary lambda-terms, Algebraic logic for classical conjunction and disjunction, The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\), A game semantics for linear logic, Decision problems for propositional linear logic, Nonmodal classical linear predicate logic is a fragment of intuitionistic linear logic, Bounded linear logic: A modular approach to polynomial-time computability, Modal companions of intermediate propositional logics, Proof nets sequentialisation in multiplicative linear logic, The logic of structures, Modal translations in substructural logics, On the expressiveness of interaction, Gödel's system \(\mathcal T\) revisited, Functional interpretations of linear and intuitionistic logic, The first axiomatization of relevant logic, A representation theorem for quantales, Principal types of BCK-lambda-terms, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, Linearizing intuitionistic implication, Girard couples of quantales, Resolution is cut-free, An exact correspondence between a typed pi-calculus and polarised proof-nets, Interpreting a finitary pi-calculus in differential interaction nets, On abstract resource semantics and computability logic, Automata theory based on complete residuated lattice-valued logic: Reduction and minimization, Abstract deduction and inferential models for type theory, Linearity and bisimulation, Constructive logic with strong negation is a substructural logic. II, Many concepts and two logics of algorithmic reduction, Phase semantics and Petri net interpretation for resource-sensitive strong negation, Investigations into a left-structural right-substructural sequent calculus, First-order Glue, Coherence in linear predicate logic, Plans, actions and dialogues using linear logic, Displaying and deciding substructural logics. I: Logics with contraposition, Light linear logic, \(\supset\)E is admissible in ``true relevant arithmetic, Reaction graph, Representing scope in intuitionistic deductions, Let's plan it deductively!, Usage counting analysis for lazy functional languages, Typed lambda calculi and applications. 9th international conference, TLCA 2009, Brasilia, Brazil, July 1--3, 2009. Proceedings, A note on Trillas' CHC models, Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions, A trace-based model for multiparty contracts, On the algebraic structure of declarative programming languages, Focusing and polarization in linear, intuitionistic, and classical logics, Automata theory based on complete residuated lattice-valued logic: Pushdown automata, The quantic conuclei on quantales, Automata theory based on complete residuated lattice-valued logic: a categorical approach, Quantum implicit computational complexity, Strong normalization property for second order linear logic, Linear logic by levels and bounded time complexity, Automated reasoning and nonclassical logics: Introduction, A non-deterministic view on non-classical negations, Gentzen-type methods for bilattice negation, Interactive observability in Ludics: the geometry of tests, Current trends in substructural logics, The eco-cognitive model of abduction. II. Irrelevance and implausibility exculpated, Bunched sequential information, A semantic account of strong normalization in linear logic, Computation by interaction for space-bounded functional programming, A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization, Free \(Q\)-algebras., Category theory, logic and formal linguistics: some connections, old and new, Relational semantics for full linear logic, Formal ontologies and coherent spaces, Dynamic spaces in concurrent constraint programming, A logic of separating modalities, On derivations of quantales, A mathematical theory of resources, Topological representation and quantic separation axioms of semi-quantales, Interaction graphs: graphings, A micrological study of negation, Static typing for a substructural lambda calculus, Proof systems and transformation games, Coalgebras, Chu spaces, and representations of physical systems, Phase semantics and decidability of elementary affine logic, Strong normalisation in the \(\pi\)-calculus, Ternary relations and relevant semantics, Naive \textit{modus ponens}, Big toy models. Representing physical systems as Chu spaces, Displacement logic for anaphora, Non-commutative logical algebras and algebraic quantales, Temporal BI: proof system, semantics and translations, What is relevance logic?, Modeling linear logic with implicit functions, Self-referentiality of Brouwer-Heyting-Kolmogorov semantics, Interpreting quantum parallelism by sequents, Figures of dialogue: a view from ludics, Light linear logics with controlled weakening: expressibility, confluent strong normalization, A relational semantics for parallelism and non-determinism in a functional setting, Visible acyclic differential nets. I: Semantics, The Scott model of linear logic is the extensional collapse of its relational model, An approach to innocent strategies as graphs, Resource modalities in tensor logic, Proof and refutation in MALL as a game, Cut elimination and strong separation for substructural logics: an algebraic approach, A minimal classical sequent calculus free of structural rules, Light Dialectica revisited, The relational model is injective for multiplicative exponential linear logic (without weakenings), A focused approach to combining logics, Deep inference and probabilistic coherence spaces, Grishin algebras and cover systems for classical bilinear logic, Contextual deduction theorems, Bounded memory Dolev-Yao adversaries in collaborative systems, A prismoid framework for languages with resources, Quantum computation: from a programmer's perspective, Linearity and iterator types for Gödel's system \(\mathcal T\), The categorical imperative: category theory as a foundation for deontic logic, A logical calculus for controlled monotonicity, Logical consequence and the paradoxes, The one-variable fragment of \(\mathrm T_\to\), Recovering quantum logic within an extended classical framework, Representation theorems for \(Q\)-algebras, Forum: A multiple-conclusion specification logic, The largest cartesian closed category of stable domains, The undecidability of simultaneous rigid E-unification, Quasi-prime algebraic domains, Petri nets and bisimulation, On maximal stable functions, Nonsymmetric \(^{\ast}\)-autonomous categories, Interpolants, cut elimination and flow graphs for the propositional calculus, Weakly distributive categories, A double deduction system for quantum logic based on natural deduction, An alternative linear semantics for allowed logic programs, Interpreting quantum logic as a pragmatic structure, On the unity of logic, Linear logic, coherence and dinaturality, A logical view of composition, Computational interpretations of linear logic, Using typed lambda calculus to implement formal systems on a machine, Automata theory based on complete residuated lattice-valued logic: Turing machines, Proving concurrent constraint programming correct, revisited, Logic and grammar, Preface to the special volume, A semantic measure of the execution time in linear logic, Correctness of linear logic proof structures is NL-complete, A linear algorithm for MLL proof net correctness and sequentialization, Intuitionistic differential nets and lambda-calculus, Linear logic as a tool for planning under temporal uncertainty, Collaborative planning with confidentiality, Structure of left-continuous triangular norms with strong induced negations. III: Construction and decomposition, Nuclei and conuclei on residuated lattices, Type inference for light affine logic via constraints on words, Disjunction property and complexity of substructural logics, Probabilistic coherence spaces as a model of higher-order probabilistic computation, Categorical relationships between Goguen sets and ``two-sided categorical models of linear logic, Coherent phase spaces. Semiclassical semantics, Polarized and focalized linear and classical proofs, A framework for proof systems, A new face of the branching recurrence of computability logic, Interaction graphs: multiplicatives, Binary quantum logic and generating semigroups, Relating state-based and process-based concurrency through linear logic (full-version), Fine-grained concurrency with separation logic, N.A. Vasil'ev's logical ideas and the categorical semantics of many-valued logic, Session-based concurrency, declaratively, Logic and majority voting, Comparing hierarchies of types in models of linear logic, (Optimal) duplication is not elementary recursive, Softness of MALL proof-structures and a correctness criterion with Mix, The differential lambda-calculus, MELL in the calculus of structures, Bifibrations of polycategories and classical linear logic, Polarized games, Finiteness spaces and generalized power series, The undecidability of proof search when equality is a logical connective, Logical foundations for hybrid type-logical grammars, Natural deduction for intuitionistic linear logic, Communicating finite state machines and an extensible toolchain for multiparty session types, Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus, Sequent reconstruction in LLM -- A sweepline proof, Basing sequent systems on exclusive-or, Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs, Default reasoning by deductive planning, Asynchronous communication model based on linear logic, Petri nets, Horn programs, linear logic and vector games, On \(\text{NP}\)-completeness in linear logic, Some lattice models of bilinear logic, Relations and non-commutative linear logic, Semantics of quantum programming languages: Classical control, quantum control, Coproduct and amalgamation of deductive systems by means of ordered algebras, Linear Läuchli semantics, Linear logic for nets with bounded resources, Linear logic automata, A linear conservative extension of Zermelo-Fraenkel set theory, Extending Lambek grammars to basic categorial grammars, Fibred semantics for feature-based grammar logic, Free algebras corresponding to multiplicative classical linear logic and some of its extensions, Categorical shape theory as a formal language for pattern recognition?, Some general results about proof normalization, The explosion calculus, A category equivalence for odd Sugihara monoids and its applications, The taming of recurrences in computability logic through cirquent calculus. I, Simple free star-autonomous categories and full coherence, A type-assignment of linear erasure and duplication, Proofs and surfaces, A categorical model of predicate linear logic, Linear logic in computer science, From QBFs to \textsf{MALL} and back via focussing, A restricted fragment of the Lambek calculus with iteration and intersection operations, An algebraic correctness criterion for intuitionistic multiplicative proof-nets, From multiple sequent for additive linear logic to decision procedures for free lattices, Variations on mobile processes, Game-theoretic analysis of call-by-value computation, The name discipline of uniform receptiveness, A specification structure for deadlock-freedom of synchronous processes, Paraconsistency in classical logic, On phase semantics and denotational semantics in multiplicative-additive linear logic, A fresh view of linear logic as a logical framework, Factorization in call-by-name and call-by-value calculi via linear logic, Generalized bounded linear logic and its categorical semantics, Focused proof-search in the logic of bunched implications, Adjoint reactive GUI programming, The spirit of node replication, Graded modal dependent type theory, Bayesian strategies: probabilistic programs as generalised graphical models, Natural deduction bottom up, Proof nets for classical logic, Structural weakening and paradoxes, Strategic reasoning with a bounded number of resources: the quest for tractability, The MacNeille completions for residuated \(S\)-posets, Polynomial time in untyped elementary linear logic, Conflict vs causality in event structures, Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms, Fuzzy sets and formal logics, A categorical construction for the computational definition of vector spaces, Proof complexity of substructural logics, The multiplicative-additive Lambek calculus with subexponential and bracket modalities, The bang calculus revisited, A comparative study of ideals in fuzzy orders, Transactions and contracts based on reaction systems, On sheaf cohomology and natural expansions, Complexity of Lambek calculi with modalities and of total derivability in grammars, Infinitary action logic with exponentiation, \(U\)-Sets as a possibilistic set theory, Stratified coherence spaces: A denotational semantics for light linear logic, Soft linear logic and polynomial time, Focussing and proof construction, The logic of tasks, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, Soft subexponentials and multiplexing, Streams and strings in formal proofs., Structural cut elimination. I: Intuitionistic and classical logic, Games and full abstraction for FPC., Decidability of linear affine logic, Encoding linear logic with interaction combinators, Non-associative, non-commutative multi-modal linear logic, The propositional logic of elementary tasks, The additive multiboxes, Projective and injective objects in the category of quantales, Prioritise the best variation, Defining formal explanation in classical logic by substructural derivability, Frobenius quantales, Serre quantales and the Riemann-Roch theorem, Resourceful program synthesis from graded linear types, A formal model for a linear time correctness condition of proof nets of multiplicative linear logic, European Summer Meeting of the Association for Symbolic Logic, Software science view on quantum circuit algorithms, Reflectors to quantales, A Survey of the Proof-Theoretic Foundations of Logic Programming, An ecumenical notion of entailment, When programs have to watch paint dry, Constructing \(Q\)-algebras from \(Q\)-modules, Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts, A formal logic for formal category theory, Quantum B‐modules, Embedding \(\mathsf{HTLCG}\) into \(\mathsf{LCG}_\phi \), Towards substructural property-based testing, A proof of the focusing theorem via MALL proof nets, Combinatorial flows as bicolored atomic flows, Hypernormalisation in an abstract setting, A monoidal closed category of event structures, Category theory in Isabelle/HOL as a basis for meta-logical investigation, Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts, Classical (co)recursion: Mechanics, Enumerating Independent Linear Inferences, Separating Sessions Smoothly, Making first order linear logic a generating grammar, Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic, A System of Interaction and Structure III: The Complexity of BV and Pomset Logic, A linear exponential comonad in s-finite transition kernels and probabilistic coherent spaces, Complementary proof nets for classical logic, Differential 2-rigs, Bracket induction for Lambek calculus with bracket modalities, Versions of a local contraction subexponential in the Lambek calculus, The elimination of maximum cuts in linear logic and BCK logic, Structural rules and algebraic properties of intersection types, Quantitative weak linearisation, A framework for substructural type systems, Relational Models for the Lambek Calculus with Intersection and Constants, Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications, Game semantics of Martin-Löf type theory, Node Replication: Theory And Practice, Explorations in Subexponential Non-associative Non-commutative Linear Logic, DisCoCat for Donkey Sentences, Semantic Analysis of Subexponential Modalities in Distributive Non-commutative Linear Logic, Quantitative global memory, Maximally multi-focused proofs for skew non-commutative \texttt{MILL}, Structural Rules in Natural Deduction with Alternatives, Cover systems for the modalities of linear logic, Unnamed Item, Unnamed Item, Unnamed Item, Focused linear logic and the \(\lambda\)-calculus, Unnamed Item, Light linear logic, Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic, The bang calculus revisited, Free \(\mu\)-lattices, Linear logic with fixed resources, Linear logic as a logic of computations, Distributed programming with logic tuple spaces, The points and diameters of quantales, Quantum logic and linear logic, Homology of proof-nets, The conjoinability relation in Lambek calculus and linear logic, Semantics of weakening and contraction, Modalities in linear logic weaker than the exponential ``of course: Algebraic and relational semantics, The complexity of Horn fragments of linear logic, Proof strategies in linear logic, Proofs as processes, On the \(\pi\)-calculus and linear logic, On proof normalization in linear logic, Head linear reduction and pure proof net extraction, First-order linear logic without modalities is NEXPTIME-hard, Constant-only multiplicative linear logic is NP-complete, Limited reasoning in first-order knowledge bases, Reflections on ``difficult embeddings, Meeting strength in substructural logics, \(*\)-autonomous categories of bimodules, On the linear decoration of intuitionistic derivations, Continuity of left-continuous triangular norms with strong induced negations and their boundary condition, Monoidal t-norm based logic: Towards a logic for left-continuous t-norms, Semantic data modelling using linear logic, Hypersequents, logical consequence and intermediate logics for concurrency, Multiparty session types, beyond duality, Completeness results for linear logic on Petri nets, A constructive game semantics for the language of linear logic, Contraction, infinitary quantifiers, and omega paradoxes, Interaction nets and term-rewriting systems, New Curry-Howard terms for full linear logic, May I borrow your logic? (Transporting logical structures along maps), Lewis meets Brouwer: constructive strict implication, Glueing and orthogonality for models of linear logic, Exhausting strategies, joker games and full completeness for IMLL with unit, Coherence for sharing proof-nets, Encoding transition systems in sequent calculus, Chu spaces as a semantic bridge between linear logic and mathematics., Handsome proof-nets: Perfect matchings and cographs, Phase semantics for light linear logic, A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic, Ramification and causality, A linear logical framework, Operational equivalence for interaction nets., Natural deduction for bi-intuitionistic logic, Linear logic and elementary time, A theory of truthmaker content. I: Conjunction, disjunction and negation, Choreographies, logically, A semantic framework for proof evidence, Introduction to computability logic, Quantale algebras as lattice-valued quantales, The cut operation on matrix factorisations, Quine and Slater on paraconsistency and deviance, Adding logic to the toolbox of molecular biology, Naive structure, contraction and paradox, Generalized approximations of \(( \in ,\in \vee q) \)-fuzzy ideals in quantales, Some points in formal topology., Non-commutative logic. III: Focusing proofs., Domain theory for concurrency, On the decision problem for MELL, The shuffle quasimonad and modules with differentiation and integration, Normalization of N-graphs via sub-N-graphs, From cut-free calculi to automated deduction: the case of bounded contraction, Hybrid and subexponential linear logics, A partial solution to an open problem of Amadio and Curien, Modularity of proof-nets. Generating the type of a module., On the expressive power of abstract categorial grammars: Representing context-free formalisms, Paraconsistent informational logic, Combining classical logic, paraconsistency and relevance, \(\bigstar\)-autonomous lattices, Compositionality for quantitative specifications, A theory of sequentiality, Generating plans in linear logic. I: Actions as proofs, Generating plans in linear logic. II: A geometry of conjunctive actions, Proof nets of PN as graphs, A characterization theorem on the rotation construction for triangular norms, MV-algebras embedded in a CL-algebra, On the logic of unification, Poset-valued sets or how to build models for linear logics, Possible worlds and resources: The semantics of \(\mathbf{BI}\), Phase semantics for a pure noncommutative linear propositional logic, Connection methods in linear logic and proof nets construction, Efficient resource management for linear logic proof search, Proof-search in type-theoretic languages: An introduction, Chu spaces from the representational viewpoint, Turning cycles into spirals, Weight of the comprehension axiom in a theory based on logic without contractions, Interaction nets for linear logic, Proof nets, garbage, and computations, Sentential constants in systems near R, Resolution calculus for the first order linear logic, Modal logic as metalogic, Finite games for a predicate logic without contractions, Defining concurrent processes constructively, The finite model property for BCK and BCIW, An internal language for autonomous categories, An equivalence between lambda- terms, Informational interpretation of substructural propositional logics, Coherent models of proof nets, 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, Note on Deduction Theorems in contraction-free logics, A coding theoretic study of MLL proof nets, Unnamed Item, Strong Equivalence of RASP Programs, Bialgebras in Rel, An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics, A Modal BI Logic for Dynamic Resource Properties, Call-by-Value Non-determinism in a Linear Logic Type Discipline, Substructural Proofs as Automata, Unification for $$\lambda $$ -calculi Without Propagation Rules, Which Logic for the Radical Anti-realist?, Stable Philosophical Systems and Radical Anti-realism, A quantum double construction in Rel, The Prismoid of Resources, Practical Tactics for Separation Logic, On Paths-Based Criteria for Polynomial Time Complexity in Proof-Nets, Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs, Conflation Confers Concurrency, I Got Plenty o’ Nuttin’, Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less), Strong negation in intuitionistic style sequent systems for residuated lattices, A Linear Logic Programming Language for Concurrent Programming over Graph Structures, A Proof Theoretic Study of Soft Concurrent Constraint Programming, European Summer Meeting of the Association for Symbolic Logic (Logic Colloquium '88), Padova, 1988, Quantales and (noncommutative) linear logic, The Relevance of Relevance to Relevance Logic, UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS, Foundations for Reliable and Flexible Interactive Multimedia Scores, A Distributed Computing Model for Dataflow, Controlflow, and Workflow in Fractionated Cyber-Physical Systems, Debits and Credits in Petri Nets and Linear Logic, Cyclic Multiplicative Proof Nets of Linear Logic with an Application to Language Parsing, Proof-Theoretic Aspects of the Lambek-Grishin Calculus, An Epistemic Separation Logic, On Classical Nonassociative Lambek Calculus, On the Logic of Expansion in Natural Language, Computation with classical sequents, Light logics and higher-order processes, On session types and polynomial time, Linear-algebraic λ-calculus: higher-order, encodings, and confluence., On quantum lambda calculi: a foundational perspective, Build your own clarithmetic I: Setup and completeness, On linear rewriting systems for Boolean logic and some applications to proof theory, Unnamed Item, Pragmatic and dialogic interpretations of bi-intuitionism. Part I, Coherence Spaces and Uniform Continuity, The Free Exponential Modality of Probabilistic Coherence Spaces, Observed Communication Semantics for Classical Processes, Metric Reasoning About $$\lambda $$-Terms: The General Case, Cathoristic Logic, Can a Quantum Computer Run the von Neumann Architecture?, Kripke semantics for the logic of problems and propositions, Single Axioms and Axiom-Pairs for the Implicational Fragments of $$\mathbf {R}$$ R , R-Mingle, and Some Related Systems, Logical Foundations of Evidential Reasoning with Contradictory Information, Machine-Checked Proof-Theory for Propositional Modal Logics, Orthogonality and Boolean Algebras for Deduction Modulo, Realizability Proof for Normalization of Full Differential Linear Logic, Böhm’s Theorem for Resource Lambda Calculus through Taylor Expansion, Relating Computational Effects by ⊤ ⊤-Lifting, Categorial Grammars and Minimalist Grammars, Minimalist Grammars in the Light of Logic, Unnamed Item, Algebraic and Categorical Aspects of Quantales, Proof interpretations with truth, Unary Resolution: Characterizing Ptime, CHARACTERIZATION OF PROJECTIVE QUANTALES, Non-uniform (hyper/multi)coherence spaces, Conuclear images of substructural logics, Structural Analysis of Narratives with the Coq Proof Assistant, A Curry–Howard View of Basic Justification Logic, Relating Toy Models of Quantum Computation: Comprehension, Complementarity and Dagger Mix Autonomous Categories, Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic, From parametric polymorphism to models of polymorphic FPC, Enforcing Availability in Failure-Aware Communicating Systems, Unnamed Item, Cyclic Multiplicative-Additive Proof Nets of Linear Logic with an Application to Language Parsing, Undecidability of the Lambek Calculus with a Relevant Modality, Information Flow Under Budget Constraints, An implementation model of the typed λ-calculus based on Linear Chemical Abstract Machine, Non-Uniform Hypercoherences, Multiplicative Linear Logics and Fibrations, Unnamed Item, 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05, Event Domains, Stable Functions and Proof-Nets, Conformal Field Theory as a Nuclear Functor, Definability and Full Abstraction, A Fully Labelled Lambda Calculus: Towards Closed Reduction in the Geometry of Interaction Machine, A Calculus for Interaction Nets Based on the Linear Chemical Abstract Machine, Soft Linear Logic and Polynomial Complexity Classes, The Power of Closed Reduction Strategies, Kripke models for linear logic, European Summer Meeting of the Association for Symbolic Logic, Uppsala 1991, A Graph Abstract Machine Describing Event Structure Composition, Hybridizing a Logical Framework, Universal Boolean Systems, Deduction Graphs with Universal Quantification, Rewritings for Polarized Multiplicative and Exponential Proof Structures, Specifying Properties of Concurrent Computations in CLF, A Meta Linear Logical Framework, Token-passing Nets for Functional Languages, Propositions as sessions, 1998 European Summer Meeting of the Association for Symbolic Logic, The shuffle Hopf algebra and noncommutative full completeness, SN and CR for free-style LKtq: linear decorations and simulation of normalization, The finite model property for various fragments of intuitionistic linear logic, Natural 3-valued logics—characterization and proof theory, Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, Quantales, observational logic and process semantics, Some monoidal closed categories of stable domains and event structures, The theory of semi-functors, A model for syntactic control of interference, A resource aware semantics for a focused intuitionistic calculus, Temporal Structures, A new constructive logic: classic logic, Girard quantaloids, Game theoretic analysis of call-by-value computation, A proof theoretical approach to communication, The mix rule, Interpolation in fragments of classical linear logic, Games and full completeness for multiplicative linear logic, Autonomous posets and quantales, Retrieving library functions by unifying types modulo linear isomorphism, An introduction to differential linear logic: proof-nets, models and antiderivatives, The true concurrency of differential interaction nets, Execution time of λ-terms via denotational semantics and intersection types, Jump from parallel to sequential proofs: exponentials, An explicit formula for the free exponential modality of linear logic, Functions as processes, RASP and ASP as a fragment of linear logic, A computational interpretation of conceptivism, Non-normal modalities in variants of linear logic, A comparison between monoidal and substructural logics, Judgement aggregation in non-classical logics, Paraconsistent constructive logic with strong negation as a contraction-free relevant logic, Extending the Curry-Howard interpretation to linear, relevant and other resource logics, A correspondence between maximal abelian sub-algebras and linear logic fragments, A new correctness criterion for the proof nets of non-commutative multiplicative linear logics, Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity, Functional-Logic Graph Parser Combinators, Three faces of natural deduction, On Banach spaces of sequences and free linear logic exponential modality, On Recursion, Replication and Scope Mechanisms in Process Calculi, Categorial Grammars and Their Logics, Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials, Bounded polymorphism in session types, Unnamed Item, Unnamed Item, A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic, A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators, Local possibilistic logic, Unnamed Item, Unnamed Item, Unnamed Item, Bunched polymorphism, Multi-focused cut elimination, Geometry of resource interaction and Taylor–Ehrhard–Regnier expansion: a minimalist approach, A linear/producer/consumer model of classical linear logic, An Isbell duality theorem for type refinement systems, A new deconstructive logic: linear logic, Programs, Grammars and Arguments: A Personal View of some Connections between Computation, Language and Logic, Games and Definability For FPC, 1996–1997 Winter Meeting of the Association for Symbolic Logic, Some reasons for generalising domain theory, A concurrent constraint programming interpretation of access permissions, Towards a typed Geometry of Interaction, On the algebraic structure of Weihrauch degrees, Codensity Lifting of Monads and its Dual, The finite model property for various fragments of linear logic, Unnamed Item, Unnamed Item, The Art of Non-asserting: Dialogue with Nāgārjuna, Coordination: Reo, Nets, and Logic, Light Linear Logic with Controlled Weakening, Linear Logic and Lukasiewicz ℵ0- Valued Logic: A Logico-Algebraic Study, Structure of left-continuous triangular norms with strong induced negations (II) Rotation-annihilation construction, A non commutative generalization of *-autonomous lattices, On traced monoidal closed categories, When are Two Algorithms the Same?, Thick Subtrees, Games and Experiments, The Cut-Elimination Theorem for Differential Nets with Promotion, Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic, Merging Procedural and Declarative Proof, Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets, Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus, Parameterised notions of computation, Unnamed Item, The algebraic lambda calculus, Jumping Boxes, Enriching an Effect Calculus with Linear Types, Focalisation and Classical Realisability, Non-Commutative First-Order Sequent Calculus, Confluence of Pure Differential Nets with Promotion, SWITCHING GRAPHS, Towards a theory of resource: an approach based on soft exponentials, A ModalWalk Through Space, Formal verification of multi-agent systems behaviour emerging from cognitive task analysis, Affine geometric spaces in tangent categories, Unnamed Item, Unnamed Item, Multiplicative conjunction and an algebraic meaning of contraction and weakening, Unnamed Item, Resource Bisimilarity in Petri Nets is Decidable, Alias burying: Unique variables without destructive reads, Linear Dependent Type Theory for Quantum Programming Languages, True concurrency semantics for a linear logic programming language with broadcast communication, Optimal reductions in interaction systems, European Summer Meeting of the Association for Symbolic Logic, Coherence for sharing proof nets, Categorial graphs, Typing Quantum Superpositions and Measurement, A Subatomic Proof System for Decision Trees, Implication, Equivalence, and Negation, An Analytic Propositional Proof System on Graphs, The geometry of Bayesian programming, Unnamed Item, Unnamed Item, The ins and outs of Clean I/O, Semantical observations on the embedding of Intuitionistic Logic into Intuitionistic Linear Logic, Unnamed Item, Linear Exponential Comonads without Symmetry, Proof Nets, Coends and the Yoneda Isomorphism, Unnamed Item, The linear-non-linear substitution 2-monad, Pretopologies and completeness proofs, Equivalences between logics and their representing type theories, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, A categorical approach to the semantics of argumentation, Hopf algebras and linear logic, Unnamed Item, Unnamed Item, Unnamed Item, Gentzenizations of relevant logics without distribution. I, The undecidability of second order linear logic without exponentials, Reference counting as a computational interpretation of linear logic, Fibred tableaux for multi-implication logics, Strong normalization for all-style LKtq, Symmetry and Interactivity in Programming, Assertion, Denial and Non-classical Theories, (Dual) Hoops Have Unique Halving, Temporal Gödel‐Gentzen and Girard translations, Common Knowledge Logic in a Higher Order Proof Assistant, On intuitionistic proof nets with additional rewrite rules and their approximations, Adequate Sets of Temporal Connectives in CTL, The monoidal structure of Turing machines, Towards Hilbert's 24th Problem: Combinatorial Proof Invariants, Relating State-Based and Process-Based Concurrency through Linear Logic, Presheaf Models of Quantum Computation: An Outline, Dialogue Categories and Frobenius Monoids, Proof-theoretic notions for software maintenance, On the Relations between Disjunctive and Linear Logic Programming, Stochastic Lambek Categorial Grammars, A Graph-Theoretic Approach to Sequent Derivability in the Lambek Calculus, System NEL is Undecidable, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Cycling in proofs and feasibility, TYPED TIMED INPUT/OUTPUT AUTOMATA IN REAL-TIME, CYBERNETIC EXPLANATION, On geometry of interaction for polarized linear logic, High-level signatures and initial semantics, On Compositionality of Dinatural Transformations, From Petri nets to linear logic, ! and ? – Storage as tensorial strength, A Fresh Look at the λ-Calculus, A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4, On the Taylor expansion of probabilistic λ-terms, Switching Graphs, Jets and differential linear logic, Dynamic game semantics, Unnamed Item, One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity, Extensions of Lambek Calculi, The Mathematics of Text Structure, Aspects of Categorical Recursion Theory, Pomset Logic, Lilac: a functional programming language based on linear logic, Interpretations of Weak Positive Modal Logics, Connecting Sequent Calculi with Lorenzen-Style Dialogue Games, St. Alasdair on Lattices Everywhere, COMPLEXITY OF THE INFINITARY LAMBEK CALCULUS WITH KLEENE STAR, Program Verification with Separation Logic, Completeness of Nominal PROPs, Linear Logic Properly Displayed, On Lambek’s Restriction in the Presence of Exponential Modalities, The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions, On the symmetry of sequentiality, Linear domains and linear maps, Holomorphic models of exponential types in linear logic, A syntax for linear logic, YET ANOTHER FUZZY MODEL FOR LINEAR LOGIC, Non-linearity as the Metric Completion of Linearity, A completeness theorem for symmetric product phase spaces, Unnamed Item, DYNAMIC NEGATION AND NEGATIVE INFORMATION, Principal type-schemes of BCI-lambda-terms, Quantitative domains, groupoids and linear logic, Graded multicategories of polynomial-time realizers, Declarative continuations: An investigation of duality in programming language semantics, From petri nets to linear logic, Causality and true concurrency: A data-flow analysis of the Pi-Calculus, Stable bistructure models of PCF, The conservation theorem for differential nets, Proof nets for multiplicative cyclic linear logic and Lambek calculus, A public announcement separation logic, Head reduction and normalization in a call-by-value lambda-calculus, Monoidal logics: completeness and classical systems, AN ABSTRACT APPROACH TO CONSEQUENCE RELATIONS, Linear Logic Proof Games and Optimization, Encodings of Turing machines in linear logic, Cofree coalgebras and differential linear logic, Implicative algebras: a new foundation for realizability and forcing, Logic and Geometry of Agents in Agent-Based Modeling, A logical framework combining model and proof theory, NONASSOCIATIVE SUBSTRUCTURAL LOGICS AND THEIR SEMILINEAR EXTENSIONS: AXIOMATIZATION AND COMPLETENESS PROPERTIES, Partially Ordered Knowledge Sharing and Fractionated Systems in the Context of other Models for Distributed Computing, Modelling Unique and Affine Typing Using Polymorphism, Classical Structures Based on Unitaries, Extended Lambek Calculi and First-Order Linear Logic, Cyclic Extensions of Order Varieties, Proofs as Polynomials, Facts, arguments, annotations and reasoning, On Hilbert's Axiomatics of Propositional Logic, Word Order Alternation in Sanskrit via Precyclicity in Pregroup Grammars, New Developments in Environment Machines, Linear logic propositions as session types, The undecidability theorem for the Horn-like fragment of linear logic (Revisited), Proof nets and semi-star-autonomous categories, On the reification of semantic linearity, Relating reasoning methodologies in linear logic and process algebra, Semantical analysis of weak Kleene logics, Proof Checking and Logic Programming, On phase semantics and denotational semantics: The exponentials, A Formal Language for Electronic Contracts, Parsing MELL proof nets, Proofs as computations in linear logic, On categorical models of classical logic and the Geometry of Interaction, Asymptotic cyclic expansion and bridge groups of formal proofs, Sequent calculus and data fusion, A phase semantics for polarized linear logic and second order conservativity, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Domains via graphs, The logical structure of linguistic commitment. III: Brandomian scorekeeping and incompatibility, Proof theory in the abstract, Disjunctive systems and L-Domains, Prolegomena to any theory of proof simplicity, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, The Role of Structural Reasoning in the Genesis of Graph Theory, Least and Greatest Fixed Points in Linear Logic, On intuitionistic query answering in description bases, Unnamed Item, Unnamed Item, Rule-Following and the Limits of Formalization: Wittgenstein’s Considerations Through the Lens of Logic, Some Syntactic Interpretations in Different Systems of Full Lambek Calculus, MODAL LOGIC WITHOUT CONTRACTION IN A METATHEORY WITHOUT CONTRACTION, Functional Interpretations of Intuitionistic Linear Logic, Bounded Linear Logic, Revisited, Unnamed Item, Programs with continuations and linear logic, The geometry of non-distributive logics, Connection-based proof construction in linear logic, Resource-distribution via Boolean constraints, Unnamed Item, Informational logic for automated reasoning, Expansion trees with cut, Deep inference and expansion trees for second-order multiplicative linear logic, Hybrid linear logic, revisited, Subexponentials in non-commutative linear logic, Constructing weak simulations from linear implications for processes with private names, Idempotent residuated structures: Some category equivalences and their applications, CONSTRUCTIVE CLASSICAL LOGIC AS CPS-CALCULUS, Towards Ludics Programming: Interactive Proof Search, Semi-implication: A Chapter in Universal Logic, Universal Logic as a Science of Patterns, Infinitary affine proofs, The parametric continuation monad, Transcendental syntax I: deterministic case
Cites Work
