Document Open Access Logo

The Next 700 Semantics: A Research Challenge

Authors Shriram Krishnamurthi , Benjamin S. Lerner, Liam Elberty

PDF

File

Thumbnail PDF
PDF
LIPIcs.SNAPL.2019.9.pdf
  • Filesize: 478 kB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
  • Software and its engineering → Language features
  • Software and its engineering → Semantics
  • Software and its engineering → Formal language definitions
Keywords
  • Programming languages
  • desugaring
  • semantics
  • testing

Metrics

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

Abstract

Modern systems consist of large numbers of languages, frameworks, libraries, APIs, and more. Each has characteristic behavior and data. Capturing these in semantics is valuable not only for understanding them but also essential for formal treatment (such as proofs). Unfortunately, most of these systems are defined primarily through implementations, which means the semantics needs to be learned. We describe the problem of learning a semantics, provide a structuring process that is of potential value, and also outline our failed attempts at achieving this so far.

Cite As Get BibTex

Shriram Krishnamurthi, Benjamin S. Lerner, and Liam Elberty. The Next 700 Semantics: A Research Challenge. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.SNAPL.2019.9

Author Details

Shriram Krishnamurthi
  • Brown University, Providence, RI, USA
Benjamin S. Lerner
  • Northeastern University, Boston, MA, USA
Liam Elberty
  • Unaffiliated

Funding

This work was partially supported by the US National Science Foundation and Brown University while all authors were at Brown University.

Acknowledgements

The authors thank Eugene Charniak and Kevin Knight for useful conversations. The reviewers provided useful feedback that improved the presentation.

References

  1. Martin Bodin, Arthur Chargueraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith. A Trusted Mechanised JavaScript Specification. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 87-100, New York, NY, USA, 2014. ACM Press. URL: https://doi.org/10.1145/2535838.2535876.
  2. Martin Bodin, Tomás Diaz, and Éric Tanter. A Trustworthy Mechanized Formalization of R. In Proceedings of the 14th ACM SIGPLAN International Symposium on Dynamic Languages, DLS 2018, pages 13-24, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3276945.3276946.
  3. Denis Bogdanas and Grigore Roşu. K-Java: A Complete Semantics of Java. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 445-456, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2676726.2676982.
  4. Arthur Charguéraud, Alan Schmitt, and Thomas Wood. JSExplain: A double debugger for JavaScript. In The Web Conference 2018, pages 1-9, Lyon, France, April 2018. URL: https://doi.org/10.1145/3184558.3185969.
  5. William Clinger and Jonathan Rees. The Revised⁴ Report on the Algorithmic Language Scheme. ACM Lisp Pointers, 4(3), July 1991. Google Scholar
  6. Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications. http://tata.gforge.inria.fr/, 2007.
  7. 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 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), New York, NY, USA, 2015. ACM Press. Google Scholar
  8. Chucky Ellison and Grigore Rosu. An Executable Formal Semantics of C with Applications. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 533-544, New York, NY, USA, 2012. ACM. URL: https://doi.org/10.1145/2103656.2103719.
  9. Matthias Felleisen. On the Expressive Power of Programming Languages. Science of Computer Programming, 17:35-75, 1991. Google Scholar
  10. Daniele Filaretti and Sergio Maffeis. An Executable Formal Semantics of PHP. In Richard Jones, editor, ECOOP 2014 - Object-Oriented Programming, pages 567-592, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-44202-9_23.
  11. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. The Essence of JavaScript. In European Conference on Object-Oriented Programming, 2010. Google Scholar
  12. Chris Hathhorn, Chucky Ellison, and Grigore Roşu. Defining the Undefinedness of C. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 336-345, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2737924.2737979.
  13. Everett Hildenbrandt, Manasvi Saxena, Xiaoran Zhu, Nishant Rodrigues, Philip Daian, Dwight Guth, Brandon Moore, Yi Zhang, Daejun Park, Andrei Ştefănescu, and Grigore Roşu. KEVM: A complete formal semantics of the Ethereum virtual machine. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pages 204-217, July 2018. URL: https://doi.org/10.1109/CSF.2018.00022.
  14. Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin S. Lerner, and Armando Solar-Lezama. Synthesis of Recursive ADT Transformations from Reusable Templates. In Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 247-263, 2017. Google Scholar
  15. Ali Kheradmand and Grigore Roşu. P4K: A formal semantics of P4 and applications. Technical report, University of Illinois at Urbana-Champaign, April 2018. URL: http://arxiv.org/abs/1804.01468.
  16. Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, Cambridge, MA, 1990. Google Scholar
  17. Daejun Park, Andrei Stefănescu, and Grigore Roşu. KJS: A complete formal semantics of JavaScript. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 346-356, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2737924.2737991.
  18. Joe Gibbs Politz, Matt Carroll, Benjamin S. Lerner, Justin Pombrio, and Shriram Krishnamurthi. A Tested Semantics for Getters, Setters, and Eval in JavaScript. In Dynamic Languages Symposium, 2012. Google Scholar
  19. Joe Gibbs Politz, Alejandro Martinez, Mae Milano, Sumner Warren, Daniel Patterson, Junsong Li, Anand Chitipothu, and Shriram Krishnamurthi. Python: The Full Monty: A tested semantics for the Python programming language. In ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications, 2013. Google Scholar
  20. Omar Zaidan and Chris Callison-Burch. Crowdsourcing Translation: Professional Quality from Non-Professionals. In Association for Computer Linguistics, pages 1220-1229, 2011. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact