Operational methods in semantics
Résumé
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.
These lecture notes contain a selection of the material taught by the
author over several years in courses on the semantics of programming
languages, foundations of programming, compilation, and concurrency
theory.
They are oriented towards master students interested in
fundamental research in computer science. The reader is supposed to be
familiar with the main programming paradigms (imperative, functional,
object-oriented,...) and to have been exposed to the notions
of concurrency and synchronization as usually discussed in a course
on operating systems.
The reader is also expected to have attended introductory courses on
automata, formal languages, mathematical logic, and compilation of
programming languages.
Our goal is to provide a compact reference for
grasping the basic ideas of a rapidly evolving field. This means that
we concentrate on the simple cases and we give a self-contained
presentation of the proof techniques. Following this approach, we manage
to cover a rather large spectrum of topics within a coherent terminology
and to shed some light, we hope, on the connections among apparently
different formalisms.
Loading...