@article{ehrhard_introduction_2016,
title = {An introduction to {Differential} {Linear} {Logic}: proof-nets, models and antiderivatives},
shorttitle = {An introduction to {Differential} {Linear} {Logic}},
url = {http://arxiv.org/abs/1606.01642},
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.},
urldate = {2019-11-28},
journal = {arXiv:1606.01642 [cs]},
author = {Ehrhard, Thomas},
month = jun,
year = {2016},
note = {ZSCC: 0000002
arXiv: 1606.01642},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic}
}
@article{girard_linear_1987,
title = {Linear logic},
volume = {50},
issn = {0304-3975},
url = {http://www.sciencedirect.com/science/article/pii/0304397587900454},
doi = {10/cmv5mj},
abstract = {The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.},
language = {en},
number = {1},
urldate = {2019-11-26},
journal = {Theoretical Computer Science},
author = {Girard, Jean-Yves},
month = jan,
year = {1987},
note = {ZSCC: 0005505},
keywords = {Denotational semantics, Linear logic, Type theory},
pages = {1--101}
}