A Tool for Describing and Checking Natural Semantics Definitions of Programming Languages
Georgian-Vlad Saioc (Department of Computer Science Aarhus University,, Denmark), Hans H\"uttel (Department of Computer Science Aalborg University,, Denmark, Department of Computer Science University of Copenhagen, Denmark)

TL;DR
This paper introduces a pedagogical metalanguage and tool that facilitate writing, checking, and executing natural semantics definitions of programming languages, aiming to improve teaching and understanding of formal semantics.
Contribution
It presents a novel metalanguage and tool that combine natural semantics notation with automatic correctness verification, enhancing educational support for semantics development.
Findings
Students find the tool helpful for learning semantics.
The tool successfully verifies the meaningfulness of semantics definitions.
It enables execution of well-defined semantics and programs.
Abstract
Many universities have courses and projects revolving around compiler or interpreter implementation as part of their degree programmes in computer science. In such teaching activities, tool support can be highly beneficial. While there are already several tools for assisting with development of the front end of compilers, tool support tapers off towards the back end, or requires more background experience than is expected of undergraduate students. Structural operational semantics is a useful and mathematically simple formalism for specifying the behaviour of programs and a specification lends itself well to implementation; in particular big-step or natural semantics is often a useful and simple approach. However, many students struggle with learning the notation and often come up with ill-defined and meaningless attempts at defining a structural operational semantics. A survey shows…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
