Semantics of straight-line programs

Abstract

This is a monograph about a theory of programming language semantics. Programming language definitions traditionally consist of two parts, called its “syntax” and its “semantics”, respectively.

The syntax of a programming language defines which character sequences are programs in that programming language. Moreover, the syntax defines how programs written in that programming language are to be parsed. (Fortunately, syntaxes can, in turn, be defined in several distinct steps. A meaningful separation of concerns isolates, for instance, the consequences of the fact that, ultimately, each program is expressed as a linear string of characters from a finite alphabet. One step does not distinguish between programs and their parse trees and defines which parse trees belong to the language. Another step is exclusively concerned with how the parse trees belonging to the language are coded as linear strings of characters; this step settles details such as how scopes are delineated, whether there will be infix operators, etc. This monograph being about semantics, we shall not pursue the different aspects of syntax definition.)