Abstract
The first lecture began with a brief history of formal semantics for programming languages. The first high-level programming languages brought to light delicate points of semantics : the passing of arguments to functions in Algol 60, " by name " or " by value ", and the binding of variables in Lisp, with its dynamic binding semantics that would later be replaced by static binding.
Partly to clarify these delicate points, partly to facilitate reasoning about programs, the first formal semantics appeared as early as the mid 1960s, following three different styles that are still very much alive today : operational semantics, with seminal work by Landin in 1964 and many uses since 1990 ; axiomatic semantics, introduced by Floyd in 1967, and developed by Hoare, Dijkstra and co-authors during the years 1970 ; denotational semantics, introduced in simplified form by Strachey around 1965 and then mathematically based on domain theory by Scott and co-authors between 1970 and 1990.
Next, the lecture introduced the small programming language IMP, which served as the object of study in most of this year's lectures. It's an imperative language, structured into arithmetic expressions, Boolean expressions, and commands that modify integer variables. Expressions lend themselves wonderfully to Strachey-style denotational semantics: " naive ". Since commands may not terminate, their denotational semantics are more delicate ; this is why we have adopted operational semantics, with reductions as in the λ-calculus, or natural semantics, or reference interpreter semantics.
Finally, the lecture motivated the need to mechanize the semantics of realistic languages, i.e. to use the power of the machine to write and reason about these semantics. As an example of this approach, we showed how to mechanize the abstract syntax and operational semantics of the IMP language using the Coq demonstration assistant. Finally, we demonstrated equivalence results between reduction semantics, natural semantics and the reference interpreter.
