PS5 partial solutions have been posted.
PS6 solutions have been posted.
The histogram for the midterm is now avaliable.
An introduction to semantics, models, design, and implementation of programming languages. Topics include operational and denotational semantics, type systems, parameter passing, higher-order functions, dynamic vs. lexical scope, lambda calculus, laziness, exceptions, side effects, continuations, objects, and modules.
CS312 or permission of the instructor.
|[pdf] Introduction, Small-step semantics|
|2||Wed, 3||[pdf] Inductive proofs, Large-step semantics||HW1|
|4||Mon, 8||[pdf] IMP and its small-step semantics|
|5||Wed, 10||[pdf] Equivalence of small- and large-step semantics, Denotational semantics||HW2|
|7||Mon, 15||[pdf] Program analysis as non-standard denotational semantics||HW3|
|10||Mon, 22||[pdf] Introduction to axiomatic semantics|
|11||Wed, 24||[pdf] An example proof using the Hoare Rules||HW4|
|12||Fri, 26||[pdf] Weakest (Liberal) Pre-conditions and PCC|
|13||Mon, 29||[pdf] The Untyped Lambda Calculus|
|[pdf] The Simply Typed Lambda Calculus|
|16||Mon, 6||Logic Programming I (ppt)|
|17||Wed, 8||Logic Programming II (ppt)|
|18||Fri, 10||Logic Programming III (ppt)|
|19||Mon, 20||[pdf] More on the Simply Typed Lambda Calculus||HW5|
|21||Fri, 24||[pdf] Intro to Polymorphism & Subtyping|
|[pdf] Parametric Polymorphism, Refs||HW6|
|23||Wed, 12||[pdf] Exceptions|
|25||Mon, 17||[pdf] Continuations||HW7|
|26||Wed, 19||[pdf] Environments and Closures|
|28||Mon, 24||[pdf] Allocation and Garbage Collection|
|29||Mon, 31||[pdf] Overview of Objects and Classes|
These books are available in the engineering library. The Winskel book is something that I recommend looking at for additional material on operational, denotational, and axiomatic semantics. In fact, the material in the notes is drawn largely from this book.
For more information on Proof Carrying Code, see George Necula's PCC page.