Document Open Access Logo

Semantics Engineering with Concrete Syntax

Author Tijs van der Storm

PDF
Thumbnail PDF

File

OASIcs.EVCS.2023.29.pdf
  • Filesize: 1.34 MB
  • 11 pages

Document Identifiers

Author Details

Tijs van der Storm
  • Centrum Wiskunde & Informatica (CWI), Amsterdam, The Netherlands
  • University of Groningen, The Netherlands

Cite AsGet BibTex

Tijs van der Storm. Semantics Engineering with Concrete Syntax. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 29:1-29:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/OASIcs.EVCS.2023.29

Abstract

Semantics engineering tools like Redex can be used to define, explore, and debug formal definitions of programming language semantics. However, such tools are often based on abstract syntax, which makes the definition of rules and the exploration of execution traces rather unfriendly. In this paper we introduce Credex, a library in the Rascal meta-programming language for defining small-step evaluation-context semantics, where terms and matching patterns are what-you-see-is-what-you-get. Credex employs parsing for decomposing terms into context and redex. Since Rascal’s grammar formalism is based on general parsing, a non-unique decomposition of a term literally corresponds to an ambiguous parse. We demonstrate the use of Credex, detail some aspects of its implementation, and discuss three case-studies.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Semantics
  • Software and its engineering → Integrated and visual development environments
Keywords
  • Semantics engineering
  • syntax
  • parsing
  • reduction semantics

Metrics

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

References

  1. Yves Bertot. A short presentation of coq. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, pages 12-16, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  2. L. Thomas van Binsbergen, Peter D. Mosses, and Neil Sculthorpe. Executable component-based semantics. Journal of Logical and Algebraic Methods in Programming, 103:184-212, 2019. URL: https://doi.org/10.1016/j.jlamp.2018.12.004.
  3. L. Thomas van Binsbergen, Neil Sculthorpe, and Peter D. Mosses. Tool support for component-based semantics. In Companion Proceedings of the 15th International Conference on Modularity, MODULARITY Companion 2016, pages 8-11, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2892664.2893464.
  4. Claus Brabrand, Robert Giegerich, and Anders Møller. Analyzing ambiguity of context-free grammars. Science of Computer Programming, 75(3):176-191, 2010. URL: https://doi.org/10.1016/j.scico.2009.11.002.
  5. Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, and Grigore Roşu. A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture. In PLDI'19, pages 1133-1148. ACM, June 2019. URL: https://doi.org/10.1145/3314221.3314601.
  6. Sebastian Erdweg, Tijs van der Storm, and Yi Dai. Capture-avoiding and hygienic program transformations. In Richard E. Jones, editor, ECOOP'14, volume 8586 of Lecture Notes in Computer Science, pages 489-514. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44202-9_20.
  7. Sebastian Erdweg, Tijs van der Storm, Markus Völter, Meinte Boersma, Remi Bosman, William R. Cook, Albert Gerritsen, Angelo Hulshout, Steven Kelly, Alex Loh, Gabriël D. P. Konat, Pedro J. Molina, Martin Palatnik, Risto Pohjonen, Eugen Schindler, Klemens Schindler, Riccardo Solmi, Vlad A. Vergu, Eelco Visser, Kevin van der Vlist, Guido H. Wachsmuth, and Jimi van der Woning. The state of the art in language workbenches. In Martin Erwig, Richard F. Paige, and Eric Van Wyk, editors, Software Language Engineering, pages 197-217, Cham, 2013. Springer International Publishing. Google Scholar
  8. Sebastian Erdweg, Tijs van der Storm, Markus Völter, Laurence Tratt, Remi Bosman, William R. Cook, Albert Gerritsen, Angelo Hulshout, Steven Kelly, Alex Loh, Gabriël Konat, Pedro J. Molina, Martin Palatnik, Risto Pohjonen, Eugen Schindler, Klemens Schindler, Riccardo Solmi, Vlad Vergu, Eelco Visser, Kevin van der Vlist, Guido Wachsmuth, and Jimi van der Woning. Evaluating and comparing language workbenches: Existing results and benchmarks for the future. Computer Languages, Systems & Structures, 44:24-47, 2015. Special issue on the 6th and 7th International Conference on Software Language Engineering (SLE 2013 and SLE 2014). URL: https://doi.org/10.1016/j.cl.2015.08.007.
  9. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics engineering with PLT Redex. MIT Press, 2009. Google Scholar
  10. Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103(2):235-271, 1992. URL: https://doi.org/10.1016/0304-3975(92)90014-7.
  11. Jan Heering, Paul Klint, et al. Semantics of programming languages: A tool-oriented approach. SIGPLAN Notices, 35(3):39-48, 2000. Google Scholar
  12. Lennart C.L. Kats and Eelco Visser. The spoofax language workbench: Rules for declarative specification of languages and ides. SIGPLAN Not., 45(10):444-463, October 2010. URL: https://doi.org/10.1145/1932682.1869497.
  13. 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: https://doi.org/10.1145/2103656.2103691.
  14. Casey Klein, Jay A. McCarthy, Steven Jaconette, and Robert Bruce Findler. A semantics for context-sensitive reduction semantics. In APLAS'11, volume 7078 of Lecture Notes in Computer Science, pages 369-383. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25318-8_27.
  15. Paul Klint. A meta-environment for generating programming environments. ACM Trans. Softw. Eng. Methodol., 2(2):176-201, 1993. URL: https://doi.org/10.1145/151257.151260.
  16. Paul Klint, Tijs van der Storm, and Jurgen J. Vinju. Rascal: A domain specific language for source code analysis and manipulation. In Ninth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM), pages 168-177. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/SCAM.2009.28.
  17. Jacob Matthews and Robert Bruce Findler. An operational semantics for Scheme. Journal of Functional Programming, 18(01):47-86, 2008. Google Scholar
  18. Jacob Matthews, Robert Bruce Findler, Matthew Flatt, and Matthias Felleisen. A Visual Environment for Developing Context-Sensitive Term Rewriting Systems, pages 301-311. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-25979-4_21.
  19. Robert McNaughton. Parenthesis grammars. J. ACM, 14(3):490-500, July 1967. URL: https://doi.org/10.1145/321406.321411.
  20. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. Lem: Reusable engineering of real-world semantics. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, pages 175-188, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2628136.2628143.
  21. Gordon D. Plotkin. The origins of structural operational semantics. The Journal of Logic and Algebraic Programming, 60-61:3-15, 2004. Structural Operational Semantics. URL: https://doi.org/10.1016/j.jlap.2004.03.009.
  22. Gordon D. Plotkin. A structural approach to operational semantics. The Journal of Logic and Algebraic Programming, 60-61:17-139, 2004. Structural Operational Semantics. URL: https://doi.org/10.1016/j.jlap.2004.05.001.
  23. Grigore Rosu. K - a semantic framework for programming languages and formal analysis tools. In Doron Peled and Alexander Pretschner, editors, Dependable Software Systems Engineering, NATO Science for Peace and Security. IOS Press, 2017. Google Scholar
  24. Carsten Schürmann. The twelf proof assistant. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 79-83, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  25. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. Ott: Effective tool support for the working semanticist. SIGPLAN Not., 42(9):1-12, October 2007. URL: https://doi.org/10.1145/1291220.1291155.
  26. Vlad A. Vergu, Pierre Neron, and Eelco Visser. Dynsem: A DSL for dynamic semantics specification. In RTA'15, pages 365-378, 2015. URL: https://doi.org/10.4230/LIPIcs.RTA.2015.365.
  27. Yong Xiao, Amr Sabry, and Zena M. Ariola. From syntactic theories to interpreters: Automating the proof of unique decomposition. Higher Order Symbol. Comput., 14(4):387-409, December 2001. URL: https://doi.org/10.1023/A:1014408032446.
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