An introduction to differential linear logic: proof-nets, models and antiderivatives

DOI10.1017/S0960129516000372zbMATH Open1456.03097arXiv1606.01642OpenAlexW2409783831MaRDI QIDQ4577980FDOQ4577980

Authors: Thomas Ehrhard 

Publication date: 7 August 2018

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Abstract: Differential Linear Logic enriches Linear Logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for Differential Linear Logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative operation becomes available. Last we briefly describe the model of sets and relations and give a more detailed account of the model of finiteness spaces and linear and continuous functions.

Full work available at URL: https://arxiv.org/abs/1606.01642

Recommendations

• The semantics and proof theory of linear logic
• Proof-search and proof nets in mixed linear logic
• scientific article; zbMATH DE number 1361538
• scientific article; zbMATH DE number 17706
• scientific article; zbMATH DE number 5043201
• Differential logic programs: Programming methodologies and semantics
• Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic
• scientific article; zbMATH DE number 7359406
• Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic
• scientific article; zbMATH DE number 1231698

Mathematics Subject Classification ID

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

Cites Work

• Reversible, irreversible and optimal \(\lambda\)-machines
• Categorical semantics of linear logic
• Title not available (Why is that?)
• Linear logic
• The system \({\mathcal F}\) of variable types, fifteen years later
• Logical Approaches to Computational Barriers
• Computational interpretations of linear logic
• Uniformity and the Taylor expansion of ordinary lambda-terms
• The differential lambda-calculus
• Normal functors, power series and \(\lambda\)-calculus
• Title not available (Why is that?)
• Finiteness spaces
• Differential categories
• The Scott model of linear logic is the extensional collapse of its relational model
• On Köthe sequence spaces and linear logic
• The conservation theorem for differential nets
• Title not available (Why is that?)
• Linear domains and linear maps
• A call-by-name lambda-calculus machine
• The algebraic lambda calculus
• The differential \(\lambda \mu\)-calculus
• A semantics for lambda calculi with resources
• Title not available (Why is that?)
• Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic
• Confluence of Pure Differential Nets with Promotion
• Handsome proof-nets: Perfect matchings and cographs
• Title not available (Why is that?)
• A convenient differential category
• A new correctness criterion for MLL proof nets
• Full abstraction for resource calculus with tests
• Transport of finiteness structures and applications
• The Cut-Elimination Theorem for Differential Nets with Promotion
• A calculus for interaction nets based on the linear chemical abstract machine
• Realizability Proof for Normalization of Full Differential Linear Logic

Cited In (30)

• Cartesian differential categories as skew enriched categories
• Title not available (Why is that?)
• Title not available (Why is that?)
• Stabilized profunctors and stable species of structures
• Encodings of Turing machines in linear logic
• Title not available (Why is that?)
• Differential Linear Logic and Polarization
• Coherent differentiation
• Differential algebras in codifferential categories
• Title not available (Why is that?)
• Reverse AD at higher types: pure, principled and denotationally correct
• Mackey-complete spaces and power series -- a topological model of differential linear logic
• Jets and differential linear logic
• Safe session-based concurrency with shared linear state
• Exponential functions in Cartesian differential categories
• Title not available (Why is that?)
• Unifying graded linear logic and differential operators
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic
• A functorial excursion between algebraic geometry and linear logic
• A logical account for linear partial differential equations
• Template games and differential linear logic
• A deep inference system for differential linear logic
• Cofree coalgebras and differential linear logic
• Models of Linear Logic based on the Schwartz $\varepsilon$-product
• Coherent interaction graphs
• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• Automath

This page was built for publication: An introduction to differential linear logic: proof-nets, models and antiderivatives

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4577980)