Furio Honsell, Simona Ronchi Della Rocca, Alberto Pravato

Structured Operational Semantics of a fragment of the language Scheme


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.