Document Open Access Logo

Reference Mutability for DOT

Authors Vlastimil Dort , Ondřej Lhoták

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2020.18.pdf
  • Filesize: 0.49 MB
  • 28 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal language definitions
  • Software and its engineering → Object oriented languages
Keywords
  • Reference Mutability
  • Read-only References
  • DOT Calculus

Metrics

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

Abstract

Reference mutability is a type-based technique for controlling mutation that has been thoroughly studied in Java. We explore how reference mutability interacts with the features of Scala by adding it to the Dependent Object Types (DOT) calculus. Our extension shows how reference mutability can be encoded using existing Scala features such as path-dependent, intersection, and union types. We prove type soundness and the immutability guarantee provided by our calculus.

Cite As Get BibTex

Vlastimil Dort and Ondřej Lhoták. Reference Mutability for DOT. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 18:1-18:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ECOOP.2020.18

Author Details

Vlastimil Dort
  • Charles University, Prague, Czech Republic
Ondřej Lhoták
  • University of Waterloo, Canada

Funding

This work was partially supported by the Czech Science Foundation project 18-17403S, partially supported by the Mobility Fund of Charles University, and partially supported by the Charles University institutional funding project SVV 260588. This research was supported by the Natural Sciences and Engineering Research Council of Canada.

References

  1. Andrei Alexandrescu. The D programming language. Addison-Wesley, Upper Saddle River, N.J, 2009. Google Scholar
  2. Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The essence of dependent object types. 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 249-272. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_14.
  3. Nada Amin, Tiark Rompf, and Martin Odersky. Foundations of path-dependent types. In Andrew P. Black and Todd D. Millstein, editors, Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, pages 233-249. ACM, 2014. URL: https://doi.org/10.1145/2660193.2660216.
  4. Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. Deny capabilities for safe, fast actors. In Elisa Gonzalez Boix, Philipp Haller, Alessandro Ricci, and Carlos Varela, editors, Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE! 2015, Pittsburgh, PA, USA, October 26, 2015, pages 1-12. ACM, 2015. URL: https://doi.org/10.1145/2824815.2824816.
  5. Michael J. Coblenz, Whitney Nelson, Jonathan Aldrich, Brad A. Myers, and Joshua Sunshine. Glacier: transitive class immutability for java. In Sebastián Uchitel, Alessandro Orso, and Martin P. Robillard, editors, Proceedings of the 39th International Conference on Software Engineering, ICSE 2017, Buenos Aires, Argentina, May 20-28, 2017, pages 496-506. IEEE / ACM, 2017. URL: https://doi.org/10.1109/ICSE.2017.52.
  6. Vlastimil Dort and Ondřej Lhoták. Reference mutability for DOT - roDOT definitions and proofs. Technical Report D3S-TR-2020-01, Dep. of Distributed and Dependable Systems, Charles University, 2020. Google Scholar
  7. Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. Uniqueness and reference immutability for safe parallelism. In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, pages 21-40, 2012. URL: https://doi.org/10.1145/2384616.2384619.
  8. Philipp Haller and Ludvig Axelsson. Quantifying and explaining immutability in scala. In Proceedings Tenth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES@ETAPS 2017, Uppsala, Sweden, 29th April 2017, pages 21-27, 2017. URL: https://doi.org/10.4204/EPTCS.246.5.
  9. Jason Z. S. Hu and Ondřej Lhoták. Undecidability of D<: and its decidable fragments. PACMPL, 4(POPL):9:1-9:30, 2020. URL: https://doi.org/10.1145/3371077.
  10. Wei Huang, Ana Milanova, Werner Dietl, and Michael D. Ernst. ReIm & ReImInfer: checking and inference of reference immutability and method purity. In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, pages 879-896, 2012. URL: https://doi.org/10.1145/2384616.2384680.
  11. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396-450, 2001. URL: https://doi.org/10.1145/503502.503505.
  12. Ifaz Kabir and Ondřej Lhoták. κDOT: scaling DOT with mutation and constructors. In Proceedings of the 9th ACM SIGPLAN International Symposium on Scala, SCALA@ICFP 2018, St. Louis, MO, USA, September 28, 2018, pages 40-50, 2018. URL: https://doi.org/10.1145/3241653.3241659.
  13. Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins, and Michael D. Ernst. Practical pluggable types for Java. In Barbara G. Ryder and Andreas Zeller, editors, Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008, Seattle, WA, USA, July 20-24, 2008, pages 201-212. ACM, 2008. URL: https://doi.org/10.1145/1390630.1390656.
  14. Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták. A simple soundness proof for dependent object types. PACMPL, 1(OOPSLA):46:1-46:27, 2017. URL: https://doi.org/10.1145/3133870.
  15. Marianna Rapoport and Ondřej Lhoták. Mutable WadlerFest DOT. In Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs, Barcelona , Spain, June 20, 2017, pages 7:1-7:6, 2017. URL: https://doi.org/10.1145/3103111.3104036.
  16. Tiark Rompf and Nada Amin. Type soundness for dependent object types (DOT). In Eelco Visser and Yannis Smaragdakis, editors, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, pages 624-641. ACM, 2016. URL: https://doi.org/10.1145/2983990.2984008.
  17. George Steed. A principled design of capabilities in Pony. URL: https://www.ponylang.io/media/papers/a_prinicipled_design_of_capabilities_in_pony.pdf.
  18. Bjarne Stroustrup. The C++ programming language. Addison-Wesley, Upper Saddle River, NJ, 2013. Google Scholar
  19. Matthew S. Tschantz and Michael D. Ernst. Javari: adding reference immutability to Java. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA, pages 211-230, 2005. URL: https://doi.org/10.1145/1094811.1094828.
  20. Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kiezun, and Michael D. Ernst. Object and reference immutability using Java generics. In Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007, Dubrovnik, Croatia, September 3-7, 2007, pages 75-84, 2007. URL: https://doi.org/10.1145/1287624.1287637.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact