Structured Operational Semantics of a Fragment of the Language Scheme

Abstract

In this paper we give a big-step Structured Operational Semantics (SOS), in the style of Plotkin, Kahn and Milner, of a significant fragment of the functional programming language Scheme , including quote, eval, quasiquote and unquote. 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.