Computational interpretations of linear logic

DOI10.1016/0304-3975(93)90181-RzbMath0791.03003DBLPjournals/tcs/Abramsky93WikidataQ56443860 ScholiaQ56443860MaRDI QIDQ685430

Samson Abramsky

Publication date: 7 July 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

operational semantics linear logic lambda calculus typed concurrent programming Curry-Howard isomorphism intuitionistic linear logic storage allocation computation as cut-elimination concurrent process order of evaluation parallel implementation of functional programming languages

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items (90)

On the largest Cartesian closed category of stable domains. ⋮ Unnamed Item ⋮ Pattern matching as cut elimination ⋮ The complexity of Horn fragments of linear logic ⋮ A new “feasible” arithmetic ⋮ The Logic of Bunched Implications ⋮ Proofs as processes ⋮ On the \(\pi\)-calculus and linear logic ⋮ On proof normalization in linear logic ⋮ Constant-only multiplicative linear logic is NP-complete ⋮ Natural deduction for intuitionistic linear logic ⋮ Typing Quantum Superpositions and Measurement ⋮ Behavioural Analysis of Sessions Using the Calculus of Structures ⋮ Asynchronous communication model based on linear logic ⋮ Petri nets, Horn programs, linear logic and vector games ⋮ Strong normalisation in the \(\pi\)-calculus ⋮ The mix rule ⋮ Games and full completeness for multiplicative linear logic ⋮ Linear logic automata ⋮ Resource operators for \(\lambda\)-calculus ⋮ An introduction to differential linear logic: proof-nets, models and antiderivatives ⋮ The true concurrency of differential interaction nets ⋮ Foundation for quantum computing. II ⋮ Paraconsistent constructive logic with strong negation as a contraction-free relevant logic ⋮ New Curry-Howard terms for full linear logic ⋮ Unnamed Item ⋮ Human rationality challenges universal logic ⋮ A general adequacy result for a linear functional language ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Contraction-free sequent calculi for intuitionistic logic ⋮ Visible acyclic differential nets. I: Semantics ⋮ RELEVANCE FOR THE CLASSICAL LOGICIAN ⋮ A linear logical framework ⋮ A type-driven vector semantics for ellipsis with anaphora using Lambek calculus with limited contraction ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ A concrete model for a typed linear algebraic lambda calculus ⋮ Quantum-like logics and schizophrenia ⋮ Unnamed Item ⋮ Three faces of natural deduction ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Focused linear logic and the \(\lambda\)-calculus ⋮ Variations on mobile processes ⋮ A specification structure for deadlock-freedom of synchronous processes ⋮ The logic of message-passing ⋮ Observed Communication Semantics for Classical Processes ⋮ Linearity and iterator types for Gödel's system \(\mathcal T\) ⋮ Linear logical relations and observational equivalences for session-based concurrency ⋮ Domain theory for concurrency ⋮ Cathoristic Logic ⋮ Reference counting as a computational interpretation of linear logic ⋮ Bounded linear logic: A modular approach to polynomial-time computability ⋮ On the concurrent computational content of intermediate logics ⋮ On the largest Cartesian closed category of stable domains ⋮ Computational interpretations of linear logic ⋮ A partial solution to an open problem of Amadio and Curien ⋮ Gödel's system \(\mathcal T\) revisited ⋮ Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion ⋮ On the unity of duality ⋮ Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi ⋮ Linearizing intuitionistic implication ⋮ Cartesian closed stable categories ⋮ Linear logic propositions as session types ⋮ An exact correspondence between a typed pi-calculus and polarised proof-nets ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Connectionist computations of intuitionistic reasoning ⋮ Coordination: Reo, Nets, and Logic ⋮ Clones, closed categories, and combinatory logic ⋮ Safe session-based concurrency with shared linear state ⋮ Reductive logic, proof-search, and coalgebra: a perspective from resource semantics ⋮ Semantics for a lambda calculus for string diagrams ⋮ Exponentials as substitutions and the cost of cut elimination in linear logic ⋮ A subexponential view of domains in session types ⋮ Plans, actions and dialogues using linear logic ⋮ Reaction graph ⋮ Intersection Types for the Resource Control Lambda Calculi ⋮ An implementation model of the typed λ-calculus based on Linear Chemical Abstract Machine ⋮ Weak linearization of the lambda calculus ⋮ A concrete categorical semantics of lambda-\(\mathcal{S}\) ⋮ Proof nets, garbage, and computations ⋮ Genericity and the \(\pi\)-calculus ⋮ Structural cut elimination. I: Intuitionistic and classical logic ⋮ Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus ⋮ A Calculus for Interaction Nets Based on the Linear Chemical Abstract Machine ⋮ The Power of Closed Reduction Strategies ⋮ Lilac: a functional programming language based on linear logic ⋮ An internal language for autonomous categories ⋮ Propositions as sessions

Uses Software

Cites Work

This page was built for publication: Computational interpretations of linear logic