Document Open Access Logo

DynSem: A DSL for Dynamic Semantics Specification

Authors Vlad Vergu, Pierre Neron, Eelco Visser

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.365.pdf
  • Filesize: 430 kB
  • 14 pages

Document Identifiers

Author Details

Vlad Vergu
Pierre Neron
Eelco Visser

Cite AsGet BibTex

Vlad Vergu, Pierre Neron, and Eelco Visser. DynSem: A DSL for Dynamic Semantics Specification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 365-378, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.RTA.2015.365

Abstract

The formal semantics of a programming language and its implementation are typically separately defined, with the risk of divergence such that properties of the formal semantics are not properties of the implementation. In this paper, we present DynSem, a domain-specific language for the specification of the dynamic semantics of programming languages that aims at supporting both formal reasoning and efficient interpretation. DynSem supports the specification of the operational semantics of a language by means of statically typed conditional term reduction rules. DynSem supports concise specification of reduction rules by providing implicit build and match coercions based on reduction arrows and implicit term constructors. DynSem supports modular specification by adopting implicit propagation of semantic components from I-MSOS, which allows omitting propagation of components such as environments and stores from rules that do not affect those. DynSem supports the declaration of native operators for delegation of aspects of the semantics to an external definition or implementation. DynSem supports the definition of auxiliary meta-functions, which can be expressed using regular reduction rules and are subject to semantic component propagation. DynSem specifications are executable through automatic generation of a Java-based AST interpreter.
Keywords
  • programming languages
  • dynamic semantics
  • reduction semantics
  • semantics engineering
  • IDE
  • interpreters
  • modularity

Metrics

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

References

  1. Casper Bach Poulsen and Peter D. Mosses. Generating specialized interpreters for modular structural operational semantics. In Proceedings of the 23rd international symposium on Logic Based Program Synthesis and Transformation, LOPSTR, 2013. Google Scholar
  2. Lorenzo Bettini. A dsl for writing type systems for xtext languages. In Christian W. Probst and Christian Wimmer, editors, Proceedings of the 9th International Conference on Principles and Practice of Programming in Java, PPPJ 2011, Kongens Lyngby, Denmark, August 24-26, 2011, pages 31-40. ACM, 2011. Google Scholar
  3. Lorenzo Bettini. Implementing java-like languages in xtext with xsemantics. In Sung Y. Shin and José Carlos Maldonado, editors, Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC '13, Coimbra, Portugal, March 18-22, 2013, pages 1559-1564. ACM, 2013. Google Scholar
  4. Denis Bogdanas and Grigore Rosu. K-java: A complete semantics of java. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 445-456. ACM, 2015. Google Scholar
  5. Koen Claessen and John Hughes. Quickcheck: a lightweight tool for random testing of haskell programs. In ICFP, pages 268-279, 2000. Google Scholar
  6. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007. Google Scholar
  7. Chucky Ellison and Grigore Rosu. An executable formal semantics of C with applications. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 533-544. ACM, 2012. Google Scholar
  8. Matthias Felleisen, Robby Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. MIT Press, 2009. Google Scholar
  9. Matthew Flatt. Plt. reference: Racket. Technical report, Technical Report PLT-TR-2010-1, PLT Inc., 2010. Google Scholar
  10. Gilles Kahn. Natural semantics. In Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing, editors, STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings, volume 247 of Lecture Notes in Computer Science, pages 22-39. Springer, 1987. Google Scholar
  11. Lennart C. L. Kats and Eelco Visser. The Spoofax language workbench: rules for declarative specification of languages and IDEs. In William R. Cook, Siobhán Clarke, and Martin C. Rinard, editors, Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, pages 444-463, Reno/Tahoe, Nevada, 2010. ACM. Google Scholar
  12. 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, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 285-296. ACM, 2012. Google Scholar
  13. Sheng Liang, Paul Hudak, and Mark P. Jones. Monad transformers and modular interpreters. In POPL, pages 333-343, 1995. Google Scholar
  14. Robin Milner, Mads Tofte, and Robert Harper. Definition of standard ML. MIT Press, 1990. Google Scholar
  15. Peter D. Mosses. Modular structural operational semantics. Journal of Logic and Algebraic Programming, 60-61:195-228, 2004. Google Scholar
  16. Peter D. Mosses and Mark J. New. Implicit propagation in structural operational semantics. Electronic Notes in Theoretical Computer Science, 229(4):49-66, 2009. Google Scholar
  17. Pierre Neron, Andrew Tolmach, Eelco Visser, and Guido Wachsmuth. A theory of name resolution. In Jan Vitek, editor, Programming Languages and Systems, volume 9032 of Lecture Notes in Computer Science, pages 205-231. Springer Berlin Heidelberg, 2015. Google Scholar
  18. Danvy Olivier, Nielsen, and Lasse R. Refocusing in reduction semantics. 2004. Google Scholar
  19. Mikael Pettersson. Compiling Natural Semantics, volume 1549 of Lecture Notes in Computer Science. Springer, 1999. Google Scholar
  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. Google Scholar
  21. Eelco Visser. Meta-programming with concrete object syntax. In Don S. Batory, Charles Consel, and Walid Taha, editors, Generative Programming and Component Engineering, ACM SIGPLAN/SIGSOFT Conference, GPCE 2002, Pittsburgh, PA, USA, October 6-8, 2002, Proceedings, volume 2487 of Lecture Notes in Computer Science, pages 299-315. Springer, 2002. Google Scholar
  22. Eelco Visser, Guido Wachsmuth, Andrew P. Tolmach, Pierre Neron, 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! 2014, Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, part of SLASH '14, Portland, OR, USA, October 20-24, 2014, pages 95-111. ACM, 2014. Google Scholar
  23. Xtext documentation. http://www.eclipse.org/Xtext/documentation/2.6.0/Xtext, 2014.
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