Semantic Models for Programming Languages (Com S 641)

This page gives access to information about the course offerings of ``Semantics of Programming Languages'' as taught in Spring 2000 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.


Overview

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 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. In 1998 we used David Schmidt's book The Structure of Typed Programming Languages (MIT Press, 1994); and studied the design of languages and type systems for them, using denotational semantics to help validate the soundness of the type systems.

In Spring 2000 will use Abadi and Cardelli's A Theory of Objects (Springer-Verlag, 1996) to study operational semantics and type theory for object-oriented programming.

Course Description

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.

Administrative Information

Com S 641, ``Semantics of Programming Languages,'' is usually taken by advanced graduate students. The class has a ``lecture'' that meets 2 times a week, for 75 minutes a time. There are usually 30 lecture meetings in a semester. The course carries 3 credit hours.

The course is only offered every other year.

Prerequisites

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:

These skills will certainly not be the focus of Com S 641, but they will be useful as building blocks for more specific tasks. If you have other facility with mathematical logic, and if you are familiar with context-free grammars, that should be enough. The skills taught in Com S 541 relevant to Com S 641 include the ability to: The background in semantics and programming you may have from Com S 541 will be sufficient.

Objectives

In general terms the essential objectives for Com S 641, Spring 2000, 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.

Understanding the semantics of major features of object-oriented programming languages is necessary both to use such features and to design new languages. For example, if you want to program in an object-oriented language you need to understand inheritance and message passing. A better understanding of such features, may help you to better program, reason about, and debug your programs. Formal methods (specification and verification) are becoming increasingly important at many companies, and a deep understanding of the semantics of programming languages is a great help in using formal methods. Without understanding the semantics of such features, you may also have difficulty discussing programming language ideas with others, and will have difficulty in reading the technical literature. If you are planning in specializing in some other area of computer science, you may someday need to read some of the literature on programming languages, either to use results from programming languages, or to apply ideas from your area to programming language research.

Type declarations are a simple form of formal specification, and type checking is a simple, automatic form of program verification. Type checking is believed to be of great help in programming, because it catches errors before a program is run, and type information is used heavily in optimizing compilers to improve generated code. The techniques of type checking can also be applied by hand in dynamically typed languages (like Smalltalk, LISP, or Scheme), and can be used for other purposes (other kinds of static analysis). These techniques are a hot topic of research, and have been so for years. Type systems of programming languages have a deep connection to logic (the Curry-Howard isomorphism). Studying type systems and paying attention to type issues in language design seems to help organize and regularize a language design.

The study of formal semantic description techniques, we believe, helps solidify your understanding of major programming language features. Such techniques are also a valuable tool for language designers. They add precision to descriptions and can be used to help prevent ambiguity. They can also be used to reason about properties of a design, such as whether the design is secure, or whether parts of the language are not useful. But more important, a mathematical model of a language or system can reveal new and interesting possibilities for language features, or the simplification of features. Primitives such as procedure closures, monitors, and continuations first emerged as the result of semantic descriptions. Formal description techniques can also aid in judging language designs, by revealing hidden interactions between features, and by giving you a sense of how simple or complex the design is.

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.

Textbooks

The required text is A Theory of Objects by Martín Abadi and Luca Cardelli (Springer-Verlag, 1996).

We will also read articles from the literature.

Syllabus

The syllabus tells when we plan to discuss various topics. The ``when'' is specified below by class meeting numbers (a count of the ``lectures'').


Last update $Date: 2002/01/04 23:02:48 $
Gary T. Leavens
229 Atanasoff Hall
Department of Computer Science, Iowa State University
Ames, Iowa 50011-1040 USA