Document Open Access Logo

Modelling Coeffects in the Relational Semantics of Linear Logic

Authors Flavien Breuvart, Michele Pagani

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.567.pdf
  • Filesize: 0.58 MB
  • 15 pages

Document Identifiers

Author Details

Flavien Breuvart
Michele Pagani

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.CSL.2015.567

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.
Keywords
  • relational semantics
  • bounded linear logic
  • lambda calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. Linear lambda-calculus and categorical models revisited. In E. Börger, G. Jäger, H. Kleine Büning, S. Martini, and M. Richter, editors, Proceedings of the Sixth Workshop on Computer Science Logic, pages 61-84. Springer Verlag, 1993. Google Scholar
  2. Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Proceedings of ESOP 2014, volume 8410 of LNCS, pages 351-370. Springer, 2014. Google Scholar
  3. Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. Exponentials with infinite multiplicities. In A. Dawar and H. Veith, editors, Proceedings of CSL 2010, volume 6247 of LNCS, pages 170-184, 2010. Google Scholar
  4. Ugo Dal Lago and Marco Gaboardi. Linear dependent types and relative completeness. In Proceedings of LICS 2011, pages 133-142. IEEE, 2011. Google Scholar
  5. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. In R. Giacobazzi and R. Cousot, editors, Proceedings of POPL 2013, pages 357-370. ACM, 2013. Google Scholar
  6. Dan R. Ghica and Alex I. Smith. Bounded linear types in a resource semiring. In Z. Shao, editor, Proceedings of ESOP 2014, volume 8410 of LNCS, pages 331-350. Springer, 2014. Google Scholar
  7. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  8. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci., 97(1):1-66, April 1992. Google Scholar
  9. Charles Grellois and Paul-André Melliès. An infinitary model of linear logic. In Proceedings of FoSSaCS 2015, volume 9034 of LNCS, pages 41-55. Springer, 2015. Google Scholar
  10. Paul-Andre Mellies. The parametric continuation monad. Mathematical Structures in Computer Science, Festschrift in honor of Corrado Böhm for his 90th birthday, 2013. Google Scholar
  11. Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic. In S. Albers, A. Marchetti-Spaccamela, Y. Matias, S. E. Nikoletseas, and W. Thomas, editors, Proceedings of ICALP 2009, pages 247-260, 2009. Google Scholar
  12. Tomas Petricek, Dominic Orchard, and Alan Mycroft. Coeffects: unified static analysis of context-dependence. In Proceedings of International Conference on Automata, Languages, and Programming - Volume Part II, ICALP, 2013. Google Scholar
  13. Tomas Petricek, Dominic Orchard, and Alan Mycroft. Coeffects: A calculus of context-dependent computation. In Proceedings of International Conference on Functional Programming, ICFP, 2014. Google Scholar
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 Imprint Privacy Contact