An introduction to differential linear logic: proof-nets, models and antiderivatives
From MaRDI portal
Publication:4577980
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.
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
Cites work
- A calculus for interaction nets based on the linear chemical abstract machine
- A call-by-name lambda-calculus machine
- A convenient differential category
- A new correctness criterion for MLL proof nets
- A semantics for lambda calculi with resources
- Categorical semantics of linear logic
- Computational interpretations of linear logic
- Confluence of Pure Differential Nets with Promotion
- Differential categories
- Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic
- Finiteness spaces
- Full abstraction for resource calculus with tests
- Handsome proof-nets: Perfect matchings and cographs
- scientific article; zbMATH DE number 2185654 (Why is no real title available?)
- scientific article; zbMATH DE number 4058907 (Why is no real title available?)
- scientific article; zbMATH DE number 1487844 (Why is no real title available?)
- scientific article; zbMATH DE number 2134913 (Why is no real title available?)
- scientific article; zbMATH DE number 3367095 (Why is no real title available?)
- Linear domains and linear maps
- Linear logic
- Logical Approaches to Computational Barriers
- Normal functors, power series and -calculus
- On Köthe sequence spaces and linear logic
- Realizability Proof for Normalization of Full Differential Linear Logic
- Reversible, irreversible and optimal \(\lambda\)-machines
- The algebraic lambda calculus
- The conservation theorem for differential nets
- The Cut-Elimination Theorem for Differential Nets with Promotion
- The differential \(\lambda \mu\)-calculus
- The differential lambda-calculus
- The Scott model of linear logic is the extensional collapse of its relational model
- The system \({\mathcal F}\) of variable types, fifteen years later
- Transport of finiteness structures and applications
- Uniformity and the Taylor expansion of ordinary lambda-terms
Cited in
(49)- Differential algebras in codifferential categories
- Exponential functions in Cartesian differential categories
- Reverse AD at higher types: pure, principled and denotationally correct
- Higher-order distributions for differential linear logic
- Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic
- Differential Linear Logic and Polarization
- Mackey-complete spaces and power series -- a topological model of differential linear logic
- scientific article; zbMATH DE number 7003195 (Why is no real title available?)
- Jets and differential linear logic
- Coherent interaction graphs
- Why \textsf{FHilb} is not an interesting (co)differential category
- scientific article; zbMATH DE number 7471682 (Why is no real title available?)
- An application of parallel cut elimination in unit-free multiplicative linear logic to the Taylor expansion of proof nets
- Differentials and distances in probabilistic coherence spaces
- Differentials and distances in probabilistic coherence spaces
- Modules over monads and operational semantics (expanded version)
- scientific article; zbMATH DE number 7204432 (Why is no real title available?)
- Encodings of Turing machines in linear logic
- Cofree coalgebras and differential linear logic
- A logical account for linear partial differential equations
- scientific article; zbMATH DE number 7407795 (Why is no real title available?)
- Models of Linear Logic based on the Schwartz \varepsilon-product
- scientific article; zbMATH DE number 7089070 (Why is no real title available?)
- scientific article; zbMATH DE number 5043201 (Why is no real title available?)
- Coherent differentiation
- Safe session-based concurrency with shared linear state
- Stabilized profunctors and stable species of structures
- Unifying graded linear logic and differential operators
- A functorial excursion between algebraic geometry and linear logic
- Template games and differential linear logic
- A deep inference system for differential linear logic
- An ultrametric for Cartesian differential categories for Taylor series convergence
- Free commutative monoids in homotopy type theory
- Additive enrichment from coderelictions
- The difference -calculus: a language for difference categories
- A profunctorial Scott semantics
- Tropical mathematics and the lambda-calculus I: metric and differential analysis of effectful programs
- Infinitary cut-elimination via finite approximations
- Unifying graded linear logic and differential operators
- Böhm and Taylor for all!
- Laplace distributors and Laplace transformations for differential categories
- Properties and characterisations of cofree Cartesian differential categories
- Combining fixpoint and differentiation theory
- Coherent Taylor expansion as a bimonad
- An axiomatics and a combinatorial model of creation/annihilation operators
- From differential linear logic to coherent differentiation
- Analytical differential calculus with integration
- Derivations as algebras
- Cartesian differential categories as skew enriched categories
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)
