An introduction to Differential Linear Logic: proof-nets, models and antiderivatives

2016/06/06 by Thomas Ehrhard, Ehrhard, Thomas · 2 citations
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO

paper · pdf · doi:10.48550/arxiv.1606.01642

arxiv created 2016/06/06 · arxiv updated 2016/06/07

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.

Cited by

• An algebra modality admitting countably many deriving transformations
• Thread and Memory-Safe Programming with CLASS

Related

• Unifying Graded Linear Logic and Differential Operators
• Convenient Antiderivatives For Differential Linear Categories
• Mackey-complete spaces and power series -- A topological model of Differential Linear Logic
• Monoidal bicategories, differential linear logic, and analytic functors
• Models of Linear Logic based on the Schwartz ε-product