Differential interaction nets

DOI10.1016/j.tcs.2006.08.003zbMath1113.03054OpenAlexW2093561140MaRDI QIDQ860836

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

linear logiclambda-calculusdifferential lambda-calculusinteraction netlambda-calculus with multiplicitiesresource lambda-calculus

Mathematics Subject Classification ID

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

Related Items

Models of Linear Logic based on the Schwartz $\varepsilon$-product ⋮ A semantic account of strong normalization in linear logic ⋮ What is a categorical model of the differential and the resource λ-calculi? ⋮ Categorical Models for Simply Typed Resource Calculi ⋮ Linear logic in normed cones: probabilistic coherence spaces and beyond ⋮ 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 ⋮ Modeling linear logic with implicit functions ⋮ Visible acyclic differential nets. I: Semantics ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ The Scott model of linear logic is the extensional collapse of its relational model ⋮ The conservation theorem for differential nets ⋮ The relational model is injective for multiplicative exponential linear logic (without weakenings) ⋮ Light logics and higher-order processes ⋮ On Banach spaces of sequences and free linear logic exponential modality ⋮ Integral categories and calculus categories ⋮ Unnamed Item ⋮ Weighted models for higher-order computation ⋮ Linearity, Control Effects, and Behavioral Types ⋮ Cofree coalgebras and differential linear logic ⋮ Geometry of resource interaction and Taylor–Ehrhard–Regnier expansion: a minimalist approach ⋮ Uniformity and the Taylor expansion of ordinary lambda-terms ⋮ Realizability Proof for Normalization of Full Differential Linear Logic ⋮ The shuffle quasimonad and modules with differentiation and integration ⋮ Properties of co-operations: diagrammatic proofs ⋮ Differential algebras in codifferential categories ⋮ Intuitionistic differential nets and lambda-calculus ⋮ A linear category of polynomial diagrams ⋮ Probabilistic coherence spaces as a model of higher-order probabilistic computation ⋮ An exact correspondence between a typed pi-calculus and polarised proof-nets ⋮ Interpreting a finitary pi-calculus in differential interaction nets ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the Meaning of Logical Completeness ⋮ The Cut-Elimination Theorem for Differential Nets with Promotion ⋮ Differential Linear Logic and Polarization ⋮ Differential categories revisited ⋮ On the Taylor expansion of probabilistic λ-terms ⋮ Confluence of Pure Differential Nets with Promotion ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Linear logic
• Uniformity and the Taylor expansion of ordinary lambda-terms
• The structure of multiplicatives
• The differential lambda-calculus
• The differential \(\lambda \mu\)-calculus
• Locus Solum: From the rules of logic to the logic of rules
• Differential categories
• A linearization of the Lambda-calculus and consequences
• A semantics for lambda calculi with resources
• On Köthe sequence spaces and linear logic
• Finiteness spaces
• Theoretical Computer Science

This page was built for publication: Differential interaction nets