Operational methods in semantics
Roberto M. Amadio
TL;DR
The notes present a coherent operational-semantics framework spanning imperative and higher-order languages, term rewriting systems, and lambda-calculus, with emphasis on how to model computations, prove termination and confluence, and relate source programs to compiled code. They develop big-step and small-step semantics for simple languages, introduce Hoare-style partial correctness, and illustrate compiler correctness via toy VM abstractions. The text then surveys termination techniques (interpretations, RPO, simplification orders) and confluence theory (critical pairs and Knuth–Bendix completion), followed by functional-programming perspectives through TRS, primitive recursion, and polynomial-time restrictions. In the lambda-calculus and its relatives, it connects higher-order computation, fixed-point phenomena, and combinatory logic, and culminates with weak reduction strategies, closures, and abstract machines, laying a foundation for implementation-oriented semantics and verification tools.
Abstract
The focus of these lecture notes is on abstract models and basic ideas and results that relate to the operational semantics of programming languages largely conceived. The approach is to start with an abstract description of the computation steps of programs and then to build on top semantic equivalences, specification languages, and static analyses. While other approaches to the semantics of programming languages are possible, it appears that the operational one is particularly effective in that it requires a moderate level of mathematical sophistication and scales reasonably well to a large variety of programming features. In practice, operational semantics is a suitable framework to build portable language implementations and to specify and test program properties. It is also used routinely to tackle more ambitious tasks such as proving the correctness of a compiler or a static analyzer.