This page gives access to information about the course offerings of ``Semantics of Programming Languages'' as taught in Fall 1990 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.
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.
The main interest will be in in how these views of semantics are connected and applied. For an example of connections, one may relate an operational semantics to an axiomatic semantics for a language to prove that the axiomatic semantics is sound and complete (or ``fully abstract'') by way of a denotational semantics. As an example of applications, one may use semantic tools such as type theory, denotational semantics, and axiomatic semantics to design new specification languages and connect them with verification techniques. Or one might design new verification techniques based on the operational semantics of a programming language.
To these topics we add a small bit of the following: type theory, category theory, the history of semantics, language design, likely topics of future research, and views on aesthetic issues.
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.
In 1990 we used David Schmidt's book Denotational Semantics: a Methodology for Language Development (Allyn and Bacon 1986), and notes from Carl Gunter that later became his book Semantics of Programming Languages (MIT Press, 1992).
We also read several papers, but today a better alternative would be to use chapters 8-10 of Schmidt's book The Structure of Typed Programming Languages (MIT Press, 1994).