Furio Honsell, Simona Ronchi Della Rocca, Alberto Pravato
Structured Operational Semantics of
a fragment of the language Scheme
Abstract
In this paper we give a big-step
{\em structured operational semantics\/} (SOS),
in the style of Plotkin, Kahn and Milner,
of a significant fragment of the functional
programming language {\em Scheme}, including
$\qq$, $\eval$, $\quasi$ and $\unq$.
The SOS formalism allows us to discuss incrementally the various features of
the language and to keep a low mathematical overhead, thus producing
a rigorous account of the semantics of a ``real'' programming language,
which nonetheless has a pedagogical value.
More specifically, we formalize four strictly
increasing fragments of Scheme, using a number of formal systems which
express the evaluation of expressions, the display of output results,
and the handling of errors.