A variety of disparate methods have traditionally been used to define the execution semantics of programming languages, to describe partial evaluation, to formalize program analysis as abstract interpretation, and to implement each of these operations in practical systems. We argue that equations and equational logic can serve to unify each of these aspects of language manipulation. The benefits of such a unified view are considerable:
Specifications of interpreters, partial evaluators, or analyzers can often be done in a modular fashion, simply by adding or removing sets of equations.
Equational systems are particularly amenable to efficient mechanical implementation, using such techniques as Knuth-Bendix completion, term graph rewriting, and compilation to machine code.
Equational semantics is very well understood. A rich body of notions and results can be brought to bear to prove useful properties of equational systems.
Implementations and formal results used for one application of equational semantics (e.g., interpreters) can often be reused or extended with ease to other settings (e.g., partial evaluators).
back to seminar homepage