Document Open Access Logo

Multi-Graded Featherweight Java

Authors Riccardo Bianchini , Francesco Dagnino , Paola Giannini , Elena Zucca

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.3.pdf
  • Filesize: 0.96 MB
  • 27 pages

Document Identifiers

Author Details

Riccardo Bianchini
  • DIBRIS, University of Genova, Italy
Francesco Dagnino
  • DIBRIS, University of Genova, Italy
Paola Giannini
  • DiSSTE, University of Eastern Piedmont, Vercelli, Italy
Elena Zucca
  • DIBRIS, University of Genova, Italy

Funding

This work was partially funded by the MUR project "T-LADIES" (PRIN 2020TL3X8X) and has the financial support of the University of Eastern Piedmont.

Acknowledgements

We thank the anonymous referees for their useful suggestions.

Cite AsGet BibTex

Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. Multi-Graded Featherweight Java. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 3:1-3:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.3

Abstract

Resource-aware type systems statically approximate not only the expected result type of a program, but also the way external resources are used, e.g., how many times the value of a variable is needed. We extend the type system of Featherweight Java to be resource-aware, parametrically on an arbitrary grade algebra modeling a specific usage of resources. We prove that this type system is sound with respect to a resource-aware version of reduction, that is, a well-typed program has a reduction sequence which does not get stuck due to resource consumption. Moreover, we show that the available grades can be heterogeneous, that is, obtained by combining grades of different kinds, via a minimal collection of homomorphisms from one kind to another. Finally, we show how grade algebras and homomorphisms can be specified as Java classes, so that grade annotations in types can be written in the language itself.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
Keywords
  • Graded modal types
  • Java

Metrics

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

References

  1. Andreas Abel and Jean-Philippe Bernardy. A unified view of modalities in type systems. Proceedings of ACM on Programming Languages, 4(ICFP):90:1-90:28, 2020. URL: https://doi.org/10.1145/3408972.
  2. Robert Atkey. Syntax and semantics of quantitative type theory. In Anuj Dawar and Erich Grädel, editors, IEEE Symposium on Logic in Computer Science, LICS 2018, pages 56-65. ACM Press, 2018. URL: https://doi.org/10.1145/3209108.3209189.
  3. Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. A Java-like calculus with user-defined coeffects. In Ugo Dal Lago and Daniele Gorla, editors, ICTCS'22 - Italian Conference on Theoretical Computer Science, volume 3284 of CEUR Workshop Proceedings, pages 66-78. CEUR-WS.org, 2022. Google Scholar
  4. Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. Multi-graded Featherweight Java. CoRR, 2023. URL: http://arxiv.org/abs/2302.07782.
  5. Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca, and Marco Servetto. Coeffects for sharing and mutation. Proceedings of ACM on Programming Languages, 6(OOPSLA):870-898, 2022. URL: https://doi.org/10.1145/3563319.
  6. Flavien Breuvart and Michele Pagani. Modelling coeffects in the relational semantics of linear logic. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, volume 41 of LIPIcs, pages 567-581. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.567.
  7. Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Zhong Shao, editor, European Symposium on Programming, ESOP 2013, volume 8410 of Lecture Notes in Computer Science, pages 351-370. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54833-8_19.
  8. Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. A graded dependent type system with a usage-aware semantics. Proceedings of ACM on Programming Languages, 5(POPL):1-32, 2021. URL: https://doi.org/10.1145/3434331.
  9. Francesco Dagnino. A meta-theory for big-step semantics. ACM Transactions on Computational Logic, 23(3):20:1-20:50, 2022. URL: https://doi.org/10.1145/3522729.
  10. Francesco Dagnino, Viviana Bono, Elena Zucca, and Mariangiola Dezani-Ciancaglini. Soundness conditions for big-step semantics. In Peter Müller, editor, European Symposium on Programming, ESOP 2020, volume 12075 of Lecture Notes in Computer Science, pages 169-196. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-44914-8_7.
  11. Ugo Dal Lago and Francesco Gavazzo. A relational theory of effects and coeffects. Proceedings of ACM on Programming Languages, 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498692.
  12. Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34(1):83-133, 1984. URL: https://doi.org/10.1016/0304-3975(84)90113-0.
  13. Werner Dietl, Sophia Drossopoulou, and Peter Müller. Generic universe types. In Erik Ernst, editor, European Conference on Object-Oriented Programming, ECOOP 2007, volume 4609 of Lecture Notes in Computer Science, pages 28-53. Springer, 2007. Google Scholar
  14. Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. Combining effects and coeffects via grading. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, ACM International Conference on Functional Programming, ICFP 2016, pages 476-489. ACM Press, 2016. URL: https://doi.org/10.1145/2951913.2951939.
  15. Dan R. Ghica and Alex I. Smith. Bounded linear types in a resource semiring. In Zhong Shao, editor, European Symposium on Programming, ESOP 2013, volume 8410 of Lecture Notes in Computer Science, pages 331-350. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54833-8_18.
  16. Colin S. Gordon. Designing with static capabilities and effects: Use, mention, and invariants (pearl). In Robert Hirschfeld and Tobias Pape, editors, European Conference on Object-Oriented Programming, ECOOP 2020, volume 166 of LIPIcs, pages 10:1-10:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2020.10.
  17. Alexander Grothendieck. Catégories fibrées et descente. In Revêtements étales et groupe fondamental, pages 145-194. Springer, 1971. Google Scholar
  18. Philipp Haller and Martin Odersky. Capabilities for uniqueness and borrowing. In Theo D'Hondt, editor, European Conference on Object-Oriented Programming, ECOOP 2010, volume 6183 of Lecture Notes in Computer Science, pages 354-378. Springer, 2010. Google Scholar
  19. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1999, pages 132-146. ACM Press, 1999. URL: https://doi.org/10.1145/320384.320395.
  20. Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer Science & Business Media, 2013. Google Scholar
  21. Daniel Marshall, Michael Vollmer, and Dominic Orchard. Linearity and uniqueness: An entente cordiale. In Ilya Sergey, editor, European Symposium on Programming, ESOP 2022, volume 13240 of Lecture Notes in Computer Science, pages 346-375. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_13.
  22. Conor McBride. I got plenty o' nuttin'. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, editors, A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 207-233. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_12.
  23. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proceedings of ACM on Programming Languages, 3(ICFP):110:1-110:30, 2019. URL: https://doi.org/10.1145/3341714.
  24. Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. Coeffects: Unified static analysis of context-dependence. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages and Programming, ICALP 2013, volume 7966 of Lecture Notes in Computer Science, pages 385-397. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_35.
  25. Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. Coeffects: a calculus of context-dependent computation. In Johan Jeuring and Manuel M. T. Chakravarty, editors, ACM International Conference on Functional Programming, ICFP 2014, pages 123-135. ACM Press, 2014. URL: https://doi.org/10.1145/2628136.2628160.
  26. Emily Riehl. Category theory in context. Courier Dover Publications, 2017. Google Scholar
  27. James Wood and Robert Atkey. A framework for substructural type systems. In Ilya Sergey, editor, European Symposium on Programming, ESOP 2022, volume 13240 of Lecture Notes in Computer Science, pages 376-402. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_14.
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