CS256  Spring 2005

Programming Languages and Semantics

Greg Morrisett
Mon & Wed 2:30-4:00pm, Maxwell Dworkin 221

Overview:

This course concerns semantic models of programs and systems and how we use those models to prove properties of programs, protocols, and languages. For example, we look at techniques for proving the input-output equivalence of two programs, or proving that a language is type-safe, or proving that an analysis is sound. Along the way, we will consider how to model advanced linguistic features such as references, closures, objects, exceptions, continuations, threads, and channels.

Regarding prerequisites, CS152 and/or CS153 is preferred.  Preferably, students will have some knowledge and experience working with a functional language, such as Scheme, ML, or Haskell. The more experience with programming in different programming languages, the better. On the theoretical side, we assume a basic proficiency in undergraduate mathematics, logic, and computer science. A basic knowledge of computability (such as Turing machines and recursive functions) and logic (that is, predicate calculus), as well as some mathematical maturity is required.

Grades will be determined by a combination of homeworks and class participation.  The homeworks will consist of a combination of written and programming exercises.  Class participation includes showing up and scribing lectures. 

There is no required text for the course, though the following books provide pieces of the material that we'll be going through.

Tentative Syllabus:


Date
 Topic
 Notes
 HW
2 Feb
 IMP/Operational Semantics
 lecture 1
7 Feb
 IMP/Rules and Induction
 lecture 2
 hw 1
9 Feb
 IMP/Denotational Semantics
 lecture 3
14 Feb
 IMP/Adequacy and Analysis
 lecture 4
 hw 2
16 Feb
 Axiomatic Semantics
 lecture 5
 hw 3
21 Feb
 NO CLASS

23 Feb
 More Axiomatic Semantics (Amal Ahmed)

28 Feb
 Simply-Typed Lambda Calculus (Matthew Fluet)
 lecture 7
 hw 4
2 Mar
 More Typed Lambda Calculus (Matthew Fluet)
 lecture 8
7 Mar
 Denotational and Algebraic Semantics
 lecture 9
9 Mar
 Exceptions, Stacks
 lecture 10
14 Mar
 CPS Conversion
 lecture 11
 hw 5
16 Mar
 Polymorphism
 lecture 12
21 Mar
 Impredicativity
 lecture 13
23 Mar
 More Impredicativity & Representation Independence
 lecture 14
28 Mar
 Spring Break

30 Mar
 Spring Break

4 Apr
 Implementing Polymorphism
 lecture 15
 hw 6
6 Apr
 F-omega
 lecture 16
11 Apr
 Recursive Functions
 lecture 17
13 Apr
 Recursive Types (I)
 lecture 18
18 Apr
 The Indexed Model
 lecture 19
20 Apr
 More Indexed Model

25 Apr
 Allocation Semantics
 lecture 21
 hw 7
27 Apr
 Labelled Transition Semantics
 lecture 22
2 May
 Substructural Typing
 lecture 23
4 May
 Spatial Logic