15-812
Fall 2000
MW 10:30-11:50
Starts on Wednesday, 13 September
Wean 4615A
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, masters-level students, and advanced undergraduates in CS, Math, or Philosophy. Some mathematical maturity will be expected. 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. This type of classification can be useful to a limited extent, but 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. In addition to its role in validating program correctness, semantics can provide a firm foundation for many activities related to programming and the design and implementation of programming languages.
We will focus on two of the most successful styles of semantic description: denotational and operational semantics. These two styles offer complementary approaches to understanding languages and programs. A denotational semantics is automatically compositional, whereas operational models may lack this property but might compensate by being intuitively easier to understand.
Following tradition, we focus on small ``core'' languages with an idealized syntax, chosen to illustrate a specific paradigm with a minimum of syntactic distraction. We will begin with a 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 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 disparate features.
The course will have a strong mathematical flavor, with additional emphasis on writing and analyzing programs. Grading will be based on homeworks, a midterm examination, and a final examination. 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.
Lecture notes handed out in class may also be obtained here (in ps format).
Look here for homework assignments.
Some macros useful for type-setting homeworks in LaTeX, designed by John Reynolds, can be found in:
Some documentation on these macros: