Search Results

Documents authored by Mirwasser, Simon


Document
Unifying Graded Linear Logic and Differential Operators

Authors: Flavien Breuvart, Marie Kerjean, and Simon Mirwasser

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)


Abstract
Linear Logic refines Classical Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which can describe the resource management or the complexity analysis of a program. From another perspective, Differential Linear Logic is an extension which allows the linearization of proofs. In this article, we merge these two directions by first defining a differential version of Graded linear logic: this is made by indexing exponential connectives with a monoid of differential operators. We prove that it is equivalent to a graded version of previously defined extension of finitary differential linear logic. We give a denotational model of our logic, based on distribution theory and linear partial differential operators with constant coefficients.

Cite as

Flavien Breuvart, Marie Kerjean, and Simon Mirwasser. Unifying Graded Linear Logic and Differential Operators. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 21:1-21:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.FSCD.2023.21,
  author =	{Breuvart, Flavien and Kerjean, Marie and Mirwasser, Simon},
  title =	{{Unifying Graded Linear Logic and Differential Operators}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.21},
  URN =		{urn:nbn:de:0030-drops-180052},
  doi =		{10.4230/LIPIcs.FSCD.2023.21},
  annote =	{Keywords: Linear Logic, Denotational Semantics, Functional Analysis, Graded Logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail