Differential interaction nets
Differential interaction nets, introduced in this paper, arise naturally as a graphical though formal presentation of commutations satisfied by morphisms associated to modalities of linear logic. Using these nets, the authors provide a linear logic account for their earlier extension of lambda-calculus with differentiation, see [\textit{T. Ehrhard} and \textit{L. Regnier}, ``The differential lambda-calculus, Theor. Comput. Sci. 309, No.~1--3, 1--41 (2003; Zbl 1070.68020)]. The authors also furnish a criterion for their net to be a correct differential net and prove this criterion to be preserved under reduction. They also show that correct nets are strongly normalizable. As the authors remark, differential nets can be viewed as a nondeterministic extension of multiplicative proof nets of linear logic, with certain exponential operations allowing several ``agents to communicate in a common ``broadcast area.
- A linearization of the Lambda-calculus and consequences
- A semantics for lambda calculi with resources
- Decidability properties of recursive types.
- Differential categories
- Finiteness spaces
- scientific article; zbMATH DE number 786495 (Why is no real title available?)
- Linear logic
- Locus solum: From the rules of logic to the logic of rules.
- On Köthe sequence spaces and linear logic
- The -calculus: A theory of mobile processes
- The differential \(\lambda \mu\)-calculus
- The differential lambda-calculus
- The structure of multiplicatives
- Uniformity and the Taylor expansion of ordinary lambda-terms
- The shuffle quasimonad and modules with differentiation and integration
- Differential algebras in codifferential categories
- Weighted models for higher-order computation
- Differential categories revisited
- A semantic account of strong normalization in linear logic
- Acyclic solos and differential interaction nets
- A hierarchy of expressiveness in concurrent interaction nets
- What is a categorical model of the differential and the resource \(\lambda \)-calculi?
- The structure of interaction
- Light logics and higher-order processes
- Linearity, control effects, and behavioral types
- Realizability Proof for Normalization of Full Differential Linear Logic
- Categorical models for simply typed resource calculi
- The Separation Theorem for Differential Interaction Nets
- Interpreting a Finitary Pi-calculus in Differential Interaction Nets
- On the Meaning of Logical Completeness
- The Cut-Elimination Theorem for Differential Nets with Promotion
- Differential Linear Logic and Polarization
- Confluence of Pure Differential Nets with Promotion
- Modeling linear logic with implicit functions
- Visible acyclic differential nets. I: Semantics
- The Scott model of linear logic is the extensional collapse of its relational model
- The relational model is injective for multiplicative exponential linear logic (without weakenings)
- Transport of finiteness structures and applications
- The true concurrency of differential interaction nets
- Order algebras: a quantitative model of interaction
- Execution time of λ-terms via denotational semantics and intersection types
- On Banach spaces of sequences and free linear logic exponential modality
- Integral categories and calculus categories
- scientific article; zbMATH DE number 7003195 (Why is no real title available?)
- Geometry of resource interaction and Taylor-Ehrhard-Regnier expansion: \textit{a minimalist approach}
- Properties of co-operations: diagrammatic proofs
- Coherent interaction graphs
- Linear logic in normed cones: probabilistic coherence spaces and beyond
- On the Taylor expansion of probabilistic λ-terms
- Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
- scientific article; zbMATH DE number 7204432 (Why is no real title available?)
- Cofree coalgebras and differential linear logic
- Models of Linear Logic based on the Schwartz \varepsilon-product
- Intuitionistic differential nets and lambda-calculus
- The conservation theorem for differential nets
- Probabilistic coherence spaces as a model of higher-order probabilistic computation
- A linear category of polynomial diagrams
- Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
- A deep inference system for differential linear logic
- An ultrametric for Cartesian differential categories for Taylor series convergence
- Graded differential categories and graded differential linear logic
- Additive enrichment from coderelictions
- Infinitary cut-elimination via finite approximations
- Unifying graded linear logic and differential operators
- Strategies as resource terms, and their categorical semantics
- Böhm and Taylor for all!
- Laplace distributors and Laplace transformations for differential categories
- Logic programming with multiplicative structures
- is for Dialectica
- An axiomatics and a combinatorial model of creation/annihilation operators
- From differential linear logic to coherent differentiation
- Extensional Taylor expansion
- Uniformity and the Taylor expansion of ordinary lambda-terms
- An exact correspondence between a typed pi-calculus and polarised proof-nets
- Interpreting a finitary pi-calculus in differential interaction nets
This page was built for publication: Differential interaction nets
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q860836)
