Search Results

Documents authored by Breuvart, Flavien

Document
DOI: 10.4230/LIPIcs.FSCD.2023.21
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}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.15
New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable

Authors: Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Working in the untyped lambda calculus, we study Morris's lambda-theory H+. Introduced in 1968, this is the original extensional theory of contextual equivalence. On the syntactic side, we show that this lambda-theory validates the omega-rule, thus settling a long-standing open problem.On the semantic side, we provide sufficient and necessary conditions for relational graph models to be fully abstract for H+. We show that a relational graph model captures Morris's observational preorder exactly when it is extensional and lambda-Konig. Intuitively, a model is lambda-Konig when every lambda-definable tree has an infinite path which is witnessed by some element of the model. Both results follow from a weak separability property enjoyed by terms differing only because of some infinite eta-expansion, which is proved through a refined version of the Böhm-out technique.
Cite as

Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.FSCD.2016.15,
  author =	{Breuvart, Flavien and Manzonetto, Giulio and Polonsky, Andrew and Ruoppolo, Domenico},
  title =	{{New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.15},
  URN =		{urn:nbn:de:0030-drops-59924},
  doi =		{10.4230/LIPIcs.FSCD.2016.15},
  annote =	{Keywords: Lambda calculus, relational models, fully abstract, B\"{o}hm-out, omega-rule}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.567
Modelling Coeffects in the Relational Semantics of Linear Logic

Authors: Flavien Breuvart and Michele Pagani

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
Various typing system have been recently introduced giving a parametric version of the exponential modality of linear logic. The parameters are taken from a semi-ring, and allow to express coeffects - i.e. specific requirements of a program with respect to the environment (availability of a resource, some prerequisite of the input, etc.). We show that all these systems can be interpreted in the relational category (Rel) of sets and relations. This is possible because of the notion of multiplicity semi-ring and allowing a great variety of exponential comonads in Rel. The interpretation of a particular typing system corresponds then to give a suitable notion of stratification of the exponential comonad associated with the semi-ring parametrising the exponential modality.
Cite as

Flavien Breuvart and Michele Pagani. Modelling Coeffects in the Relational Semantics of Linear Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 567-581, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.CSL.2015.567,
  author =	{Breuvart, Flavien and Pagani, Michele},
  title =	{{Modelling Coeffects in the Relational Semantics of Linear Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{567--581},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.567},
  URN =		{urn:nbn:de:0030-drops-54384},
  doi =		{10.4230/LIPIcs.CSL.2015.567},
  annote =	{Keywords: relational semantics, bounded linear logic, lambda calculus}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact