This page gives access to information about the course offerings of ``Semantics of Programming Languages'' as taught in Fall 1994 by Gary T. Leavens for the Department of Computer Science at Iowa State University.
This is an old offering of the course. Information about the latest offering, with links to others, is also available.
Information is available under the following headings.
Also available are the following.
This topics discussed in this course change each time it is offered. In 1990 we used notes from Carl Gunter that later became his book Semantics of Programming Languages and also studied type theory. In 1992, we used Friedman, Wand, and Haynes's (then new) book Essentials of Programming Languages, and also studied type theory and lambda Prolog. In 1994, we used a recent monograph by Wim H. Hesselink, Programs, Recursion, and Unbounded Choice (Cambridge, 1992) as the major focus of the course. The focus was on axiomatic (or predicate transformer) semantics.
The catalog description of the course is as follows:
Interpretative, denotational, and logically based models of semantics; application of semantics to program correctness, language specification, and translation. (3 credits)
Interpretative models are sometimes called ``operational'' and are exemplified by Plotkin's terminal transition systems (rewrite rules) or Landin's SECD machine (an interpreter). Denotational models are exemplified by the Scott-Strachey approach which uses functions over various domains as the meanings of programs; but in certain contexts algebraic structures are also used as denotations. Logically based models include axiomatic semantics (e.g., a Hoare logic for partial correctness) and inference systems used in the study of ``logic-oriented'' languages (such as Prolog) or type theory.
Com S 641, ``Semantics of Programming Languages,'' is usually taken by advanced graduate students. The class has a ``lecture'' that meets 3 times a week, for 50 minutes a time. There are usually 43 or 44 lecture meetings in a semester. The course carries 3 credit hours.
The course is only offered every other year.
The prerequisites are successful completion of Com S 531 (theoretical foundations) and Com S 541 (Programming Languages 1). The skills taught in Com S 531 relevant to Com S 641 include the ability to:
In general terms the essential objectives for Com S 641, Fall 1994, are as follows.
Some familiarity with formal semantic description techniques is helpful so that you can communicate the results of your work on programming language design, specification language design, or formal methods to others, and so that you can read what others have done. Formal semantic description techniques are valuable as a tool for specification and programming language designers, since they help prevent ambiguity. They can also be of use in software engineering, where they can be used to reason about properties of a design. Formal semantic description techniques can also aid in judging programming or specification language designs, by revealing hidden interactions between features, and by giving you a sense of how simple or complex the design is.
Although in my work on the semantics of subtyping I have mostly used denotational techniques, I have been impressed with the ability of authors who use axiomatic semantics to more quickly and succinctly present semantics of programming languages. I believe this is because they seem to work at a higher level of abstraction. Furthermore, the work of such authors seems closer to the practice of programming, because it is presented within a semantic framework that is closely tied to reasoning about programs. Finally, for those of us involved in the design and semantics of formal specification languages, work on axiomatic semantics has an obvious application both as a guide to what features are desirable in a specification language, and as a way of formally describing the meaning of such a specification language.
Predicate transformer semantics is a way to use verification technology to define programming languages. Each statement in a language is characterized by the way it transforms preconditions to postconditions. Dijkstra and his followers have even advocated the direct use of predicate transformers, such as the weakest precondition transformer (wp), in program development; the argument is that such predicate transformers aid calculational proofs.
The application of predicate transformer semantics to real programming languages will help you see what the capabilities and limitations of the techniques are, as well as making sure they are well understood. Limitations of current techniques point out both places to be careful in language design, and also areas where more research would be fruitful. Turning this idea on its head, one can design programming languages that are well adapted to current verification methods. (Such considerations have motivated the languages Alphard and Euclid.)
Making connections with other kinds of semantics is necessary both for a thorough evaluation of the utility of predicate transformer techniques and to appraise which semantic techniques are best for which tasks. One often needs complimentary descriptions of a programming language or specification language, both to increase confidence in the correctness of the semantics and because different kinds of techniques aid different studies. For example, operational semantics seem well-suited for studying properties of implementations; denotational semantics seem to match the way language designers think about and describe programming languages. Because denotational semantics is a good intermediate abstraction between predicate transformer semantics and operational semantics, it is important to see how to prove a predicate transformer semantics correct with respect to a denotational semantics.
The style of calculational proofs of program correctness has been advocated by Dijkstra and his followers as a way to help ensure that no mistakes are made in program proofs. I also find the discipline of developing proofs without ``pulling any rabbits out of the hat'' admirable as a way of teaching, learning, and seeking precision.
Knowing the goals and problems of programming language semantics gives you perspective on the rest of the work. It also shows possibilities for your own research and what kinds of ways that programming may be changing in the future.
The required text is Wim H. Hesselink's Programs, Recursion, and Unbounded Choice (Cambridge, 1992, ISBN 0-521-40436-3).
The recommended text is Edward Cohen's Programming in the 1990s: An Introduction to the Calculation of Programs (Springer-Verlag, 1990, ISBN 0-387-97382-6).
I also had students read articles from the literature and report on them.
The syllabus for Fall 1994 is as follows. The syllabus tells when we discussed various topics. The ``when'' is specified below by class meeting numbers (a count of the ``lectures''). Readings from Cohen's and Hesslink's books are marked with their names. We went a bit more slowly over Hesselink's book than originally planned, as we tried to ``uncover'', rather than ``cover'' it.
Meeting Readings
Numbers Topic Essential Enrichment
---------------------------------------------------------------------------
1-5 Overview/motivation [Hoare 69],
[Dijkstra 75] handouts
6 Calculation & precision Cohen 0, 1 refs. on calculation
7-10 Predicates Cohen 2, 3 [Dijkstra Scholten 90]
11-15 Development of programs Cohen 4-7 Cohen 8-13
16-24 Predicate Transformer Sem. Hesselink 0, 1
24-32 Annotation, recursion Hesselink 2
33-36 Healthiness laws Hesselink 3 [Dijkstra Scholten 90]
37-42 Semantics of recursion Hesselink 4
43-44 Summary and course eval
----------------------------------------------------------------------------
If I were to use these texts again, I'd probably go much faster over Cohen's chapters 4-7 as some of that material is also found in Hesselink, and isn't so important for a semantics course.