TY - JOUR
TI - Linear logic
AU - Girard, Jean-Yves
T2 - Theoretical Computer Science
AB - 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.
DA - 1987/01/01/
PY - 1987
DO - 10/cmv5mj
DP - ScienceDirect
VL - 50
IS - 1
SP - 1
EP - 101
J2 - Theoretical Computer Science
LA - en
SN - 0304-3975
UR - http://www.sciencedirect.com/science/article/pii/0304397587900454
Y2 - 2019/11/26/21:07:06
KW - Denotational semantics
KW - Linear logic
KW - Type theory
ER -
TY - JOUR
TI - An introduction to Differential Linear Logic: proof-nets, models and antiderivatives
AU - Ehrhard, Thomas
T2 - arXiv:1606.01642 [cs]
AB - 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.
DA - 2016/06/06/
PY - 2016
DP - arXiv.org
ST - An introduction to Differential Linear Logic
UR - http://arxiv.org/abs/1606.01642
Y2 - 2019/11/28/11:52:31
KW - Denotational semantics
KW - Differential Linear Logic
KW - Differentiation
KW - Linear logic
ER -