Document Open Access Logo

Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics

Authors Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, Eelco Visser

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2016.20.pdf
  • Filesize: 0.86 MB
  • 26 pages

Document Identifiers

Author Details

Casper Bach Poulsen
Pierre Néron
Andrew Tolmach
Eelco Visser

Cite As Get BibTex

Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, and Eelco Visser. Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 20:1-20:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ECOOP.2016.20

Abstract

Semantic specifications do not make a systematic connection between the names and scopes in the static structure of a program and memory layout, and access during its execution. In this paper, we introduce a systematic approach to the alignment of names in static semantics and memory in dynamic semantics, building on the scope graph framework for name resolution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection.

Subject Classification

Keywords
  • Dynamic semantics
  • scope graphs
  • memory layout
  • type soundness
  • operational semantics

Metrics

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

Supplementary Materials

References

  1. Arthur Charguéraud. Pretty-big-step semantics. In Matthias Felleisen and Philippa Gardner, editors, ESOP'13, volume 7792 of LNCS, pages 41-60. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37036-6_3.
  2. Martin Churchill, Peter D. Mosses, Neil Sculthorpe, and Paolo Torrini. Reusable components of semantic specifications. Transactions on Aspect-Oriented Software Development, 12:132-179, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46734-3_4.
  3. Sophia Drossopoulou and Susan Eisenbach. Java is type safe - probably. In Mehmet Aksit and Satoshi Matsuoka, editors, ECOOP'97, volume 1241 of LNCS, pages 389-418. Springer, 1997. Google Scholar
  4. Erik Ernst, Klaus Ostermann, and William R. Cook. A virtual class calculus. In J. Gregory Morrisett and Simon L. Peyton Jones, editors, POPL'06, pages 270-282. ACM, 2006. URL: http://dx.doi.org/10.1145/1111037.1111062.
  5. Matthias Felleisen. The Calculi of λ-v-cs Conversion: A Syntactic Theory of Control and State in Imperative Higher-order Programming Languages. PhD thesis, Indiana University, 1987. Google Scholar
  6. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. TOPLAS, 23(3):396-450, 2001. URL: http://dx.doi.org/10.1145/503502.503505.
  7. Gilles Kahn. Natural semantics. In Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing, editors, STACS'87, volume 247 of LNCS, pages 22-39. Springer, 1987. Google Scholar
  8. Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. Run your research: on the effectiveness of lightweight mechanization. In John Field and Michael Hicks, editors, POPL'12, pages 285-296. ACM, 2012. URL: http://dx.doi.org/10.1145/2103656.2103691.
  9. Gerwin Klein and Tobias Nipkow. A machine-checked model for a Java-like language, virtual machine, and compiler. TOPLAS, 28(4):619-695, 2006. URL: http://dx.doi.org/10.1145/1146811.
  10. Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Inf. Comput., 207(2):284-304, 2009. URL: http://dx.doi.org/10.1016/j.ic.2007.12.004.
  11. Robin Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17(3):348-375, 1978. Google Scholar
  12. J. Gregory Morrisett, Matthias Felleisen, and Robert Harper. Abstract models of memory management. In FPCA'95, pages 66-77, 1995. Google Scholar
  13. Peter D. Mosses and Mark J. New. Implicit propagation in structural operational semantics. ENTCS, 229(4):49-66, 2009. URL: http://dx.doi.org/10.1016/j.entcs.2009.07.073.
  14. Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A theory of name resolution. In Jan Vitek, editor, ESOP'15, volume 9032 of LNCS, pages 205-231. Springer, 2015. Google Scholar
  15. Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. Functional big-step semantics. In ESOP'16, volume 9632 of LNCS, pages 589-615. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49498-1_23.
  16. Gordon D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17-139, 2004. Google Scholar
  17. Casper Bach Poulsen, Pierre Néron, Andrew P. Tolmach, and Eelco Visser. Scopes describe frames: A uniform model for memory layout in dynamic semantics. Technical Report TUD-SERG-2016-010, Delft University of Technology, Programming Languages Research Group, Delft, The Netherlands, 2016. Google Scholar
  18. John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363-397, 1998. Google Scholar
  19. Tiark Rompf and Nada Amin. From F to DOT: Type soundness proofs with definitional interpreters, 2015. URL: http://arxiv.org/abs/1510.05216.
  20. Grigore Rosu and Traian-Florin Serbanuta. An overview of the K semantic framework. Journal of Logic and Algebraic Programming, 79(6):397-434, 2010. URL: http://dx.doi.org/10.1016/j.jlap.2010.03.012.
  21. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strnisa. Ott: Effective tool support for the working semanticist. Journal of Functional Programming, 20(1):71-122, 2010. URL: http://dx.doi.org/10.1017/S0956796809990293.
  22. Jeremy G. Siek. Type safety in three easy lemmas, May 2013. URL: http://siek.blogspot.co.uk/2013/05/type-safety-in-three-easy-lemmas.html.
  23. Christopher Strachey. Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, 13(1/2):11-49, 2000. Google Scholar
  24. Don Syme. Proving Java type soundness. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS, pages 83-118. Springer, 1999. Google Scholar
  25. Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A constraint language for static semantic analysis based on scope graphs. In Martin Erwig and Tiark Rompf, editors, PEPM'16, pages 49-60. ACM, 2016. URL: http://dx.doi.org/10.1145/2847538.2847543.
  26. Vlad A. Vergu, Pierre Néron, and Eelco Visser. DynSem: A DSL for dynamic semantics specification. In Maribel Fernández, editor, RTA'15, volume 36 of LIPIcs, pages 365-378. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2015.365.
  27. Eelco Visser, Guido Wachsmuth, Andrew P. Tolmach, Pierre Néron, Vlad A. Vergu, Augusto Passalaqua, and Gabriël D. P. Konat. A language designer’s workbench: A one-stop-shop for implementation and verification of language designs. In Andrew P. Black, Shriram Krishnamurthi, Bernd Bruegge, and Joseph N. Ruskiewicz, editors, Onward!'14, pages 95-111. ACM, 2014. URL: http://dx.doi.org/10.1145/2661136.2661149.
  28. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, November 1994. 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 About DROPS Imprint Privacy Contact