Treffer: Operational methods in semantics

Master
The focus of these lecture notes is on abstract models and basic ideasand results that relate to the operational semantics ofprogramming languages largely conceived. The approach is to startwith an abstract description of the computation steps of programs andthen to build on top semantic equivalences, specification languages,and static analyses. While other approaches to the semantics ofprogramming languages are possible, it appears that the operationalone is particularly effective in that it requires a moderate level ofmathematical sophistication and scales reasonably well to a largevariety of programming features. In practice, operational semanticsis a suitable framework to build portable language implementations andto specify and test program properties.It is also used routinely totackle more ambitious tasks such as proving the correctness of acompiler or a static analyzer.These lecture notes contain a selection of the material taught by theauthor over several years in courses on the semantics of programminglanguages, foundations of programming, compilation, and concurrencytheory.They are oriented towards master students interested infundamental research in computer science. The reader is supposed to befamiliar with the main programming paradigms (imperative, functional,object-oriented,...) and to have been exposed to the notionsof concurrency and synchronization as usually discussed in a courseon operating systems.The reader is also expected to have attended introductory courses onautomata, formal languages, mathematical logic, and compilation ofprogramming languages. Our goal is to provide a compact reference forgrasping the basic ideas of a rapidly evolving field. This means thatwe concentrate on the simple cases and we give a self-containedpresentation of the proof techniques. Following this approach, we manageto cover a rather large spectrum of topics within a coherent terminologyand to shed some light, we hope, on the connections among apparently different formalisms.