Starts on Wednesday, 13 September
This course can be taken as a ``starred course'' to fulfil the Programming Languages core requirement of the CMU CS Ph.D. program.
This course introduces foundational concepts and techniques of programming language semantics, and demonstrates their application in program analysis and synthesis, and their relevance in language design and implementation. We bring out the key concepts and techniques, building in the necessary mathematics and logic as we go. We aim to demonstrate the utility of a scientific approach to programming languages in answering questions about the pro's and con's of various languages, about compiler correctness, and for other practical purposes.
This course should be accessible to graduate students and masters-level students in CS, Math, or Philosophy. Some mathematical maturity will be expected. Advanced undergraduates wishing to take this course should contact the instructor for permission.
There is a wide variety of programming languages, ranging from low-level machine code and assembler to high-level languages such as C, Java, and Standard ML. A few major paradigms have been identified (e.g. ``functional'', ``imperative'', ``object-oriented'') and a particular language may belong to one or more of these. Although this type of classification can be useful to a limited extent, it is much more important to understand the relationship between program syntax (what we write) and algorithms (what happens, in abstract terms, when a program runs). This is one of the purposes of programming language semantics. A semantics for a programming language is a mathematical model that reflects the intended computational behavior of programs. To be useful, a semantics needs to be:
In addition to its role in validating program correctness, semantics can provide a firm foundation for many activities related to programming and programming languages.
As is traditional in semantics texts and research, we do not work with entire ``real'' programming languages like C and Java. Instead we focus on small ``core'' languages with an idealized (and simplified) syntax. Each core language is chosen to exhibit the features common to languages in a specific paradigm, with a minimum of syntactic distraction. In each case, we will show how a semantics can be used to analyze individual programs, to design correct programs, and to prove general laws of program equivalence that can be used to simplify programs while preserving correctness.
We will begin with a simple sequential imperative programming language, since it requires little semantic sophistication and allows us to introduce the major concepts, notation, and techniques painlessly. We then apply and generalize these ideas and techniques to a series of more complex languages. The approach is incremental, studying each feature (e.g. parallelism) in as simple a setting as possible to minimize the potential for confusion and bring out the key issues caused by the feature itself, rather than having to deal with a grab-bag language containing many logically disparate features (like parallelism and modules) and trying to disentangle.
The course will have a strong mathematical flavor, but also a strong emphasis on writing programs. Students will be expected to write programs in Standard ML. Despite its primarily functional nature, ML can be used to illustrate imperative, object-oriented, and concurrent programming issues as well as issues related to functional programming. By limiting to a single language we avoid the need to learn a new language every week. We also use ML to implement semantic definitions for other languages, thus providing a testbed facility for debugging semantic descriptions and for trying out various combinations of language features.
Grading will be based on homeworks, a midterm examination, a final examination, and (to a lesser, more informal sense) on class participation. Homework will include both written assignments and programming problems. The midterm and final will be open-book.
The course will be graded (for CS graduate students) on a pass/fail basis. Undergraduates will be assigned a letter grade.
Students are encouraged to form study groups to discuss homework problems and course material, but any work turned in for a grade must be solely the work of the individual. It is not acceptable to solve a problem collectively in a group and then write the answers up for individual submission. Copying or adaptation from a published book or article, or from previous core course documentation, is also unacceptable.
Lecture notes handed out in class may also be obtained here (in ps format).
Lecture Notes vol. 1
LaTeX source for homework 1
PS version of homework 1
Some macros useful for type-setting homeworks in LaTeX, designed by John Reynolds, can be found in:
Some documentation on these macros: