Differential interaction nets

DOI10.1016/J.TCS.2006.08.003MaRDI QIDQ860836zbMATH OpenOpenAlexFDO

Authors Thomas Ehrhard, Laurent Regnier

Publication date 9 January 2007

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

Full work available at URL https://doi.org/10.1016/j.tcs.2006.08.003

zbMATH Keywords

differential lambda-calculusinteraction netlambda-calculuslambda-calculus with multiplicitieslinear logicresource lambda-calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Intuitionistic differential nets and lambda-calculus
• The structure of interaction
• The Separation Theorem for Differential Interaction Nets
• Interaction nets for linear logic
• Visible acyclic differential nets. I: Semantics

Cites work

• 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

Cited in

(61)

• 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)