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

File

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

Document Identifiers

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

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.

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

Author Details

Casper Bach Poulsen
Pierre Néron
Andrew Tolmach
Eelco Visser

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
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact