https://doi.org/10.71352/ac.57.117
A comparison of big-step semantics definition styles
Abstract.
Formal semantics provides rigorous, mathematically precise definitions of programming languages, with which we can argue about program
behaviour and program equivalence by formal means; in particular, we can describe and verify our arguments with a proof assistant.
There are various approaches to giving formal semantics to programming languages, at different abstraction levels and applying different
mathematical machinery. In this paper we investigate some of the approaches that share their roots with traditional relational
big-step
semantics, such as (a) functional big-step semantics, (b) pretty-big-step semantics and (c) traditional natural semantics. We compare these
approaches with respect to the following criteria: executability of the semantics definition, proof complexity for essential mathematical
properties and the conciseness of expression equivalence proofs. The comparison is based on formalisations of a sequential subset of
Core Erlang, a simple functional programming language.
