Differential interaction nets

DOI10.1016/j.tcs.2006.08.003zbMath1113.03054MaRDI 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 logic; lambda-calculus; differential lambda-calculus; interaction net; lambda-calculus with multiplicities; resource lambda-calculus

Mathematics Subject Classification ID

03F52: Proof-theoretic aspects of linear logic and other substructural logics

03B40: Combinatory logic and lambda calculus

Related Items

Unnamed Item, 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, Geometry of resource interaction and Taylor–Ehrhard–Regnier expansion: a minimalist approach, Properties of co-operations: diagrammatic proofs, Unnamed Item, Cofree coalgebras and differential linear logic, Models of Linear Logic based on the Schwartz $\varepsilon$-product, The conservation theorem for differential nets, A linear category of polynomial diagrams, A semantic account of strong normalization in linear logic, 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), Intuitionistic differential nets and lambda-calculus, Probabilistic coherence spaces as a model of higher-order probabilistic computation, 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, The shuffle quasimonad and modules with differentiation and integration, Differential algebras in codifferential categories, Weighted models for higher-order computation, Differential categories revisited, What is a categorical model of the differential and the resource λ-calculi?, 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, 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

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