CS152: Principles of Programming Languages

Course topics

Introduction to Coq.
Relations, inference rules, and induction.
Syntax: concrete vs. abstract.
Operational semantics for IMP: big-step, small-step.
Denotational semantics for IMP.
Axiomatic semantics for IMP.
Case study: proof-carrying code.
Simple types.
Variables, scope, binding, and functions.
Polymorphism.
Exceptions, continuations.
Concurrency.
Pure type systems, Curry-Howard, and CiC.
Objects, classes and modules.

Assignments

Assignments will be due at 11 AM (the start of class). Please e-mail to jyang [at] eecs.harvard.edu. Late homeworks may be graded but will receive a score of 0. The lowest homework score may be dropped.

Number Assignment Due Solutions

0 Finger exercises Monday, 2.11 Desai's solutions

1 Proofs with IMP Wednesday, 2.20 IMP solutions

Project proposal Description Wednesday, 2.20

2 Denotational semantics Friday, 2.29 Abel's solutions

Finalized project proposal High-level design document,
"Hello World" program(s) Friday, 2.29

3 Simply typed lambda calculus Monday, 3.17

Midterm In class
Study guide Wednesday, 3.19
"Significant" program See below Friday, 3.21

Term paper See below Last week of classes

4 CPS Wednesday, 4.9 Seiler's solutions

5 Type inference Friday, 4.18

Final Harvard Hall 202
Study guide Tuesday, 5.20 9:15 AM

Resources

You may find this Coq Tactics Cheat Sheet helpful.
Computing with Lambda - the lambda calculus with and without types, with exceptions, with continuations, and transformed into continuation-passing style.

Term project

There will be a 2-part term project:

Pick an "unusual" language. Build something substantial in it (e.g., a web server). Submit code with documentation and some comments on the language by Friday, 3.21.
Explore history and literature surrounding language. Evaluate the language qualitatively and comparatively.

The term project has two objectives:

To introduce you to an "interesting" language with which you are unfamiliar.
To have you prove that you can digest material on your own and present the information to others in a coherent way. Communication matters.

You are encouraged to use LaTeX for your paper. There will be prizes for wackiest language, best coding project, and best writeup.

Suggested languages:

Ada Statically typed, imperative, and OO. Inspired C++'s generics.

Haskell Pure functional.

Lisp Functional language based on lambda calculus.

Modula-3 Safe language with OO, generics, multithreading, exception handling, and garbage collection.
Prolog Logic programming.

Smalltalk Pure OO.

See the History of Programming Languages wiki page for more on programming languages. It may also be useful to consult these genealogical diagrams on the history of programming languages. Come talk to us and we can give you pointers as to how to install compilers/interpreters and what sorts of programs would be appropriate for the language.

Grading

Roughly one assignment per week (drop lowest grade)	60% of grade
Two exams	10% of grade each
10 page term paper	15% of grade
Whether Prof. Morrisett likes you	5% of grade

Course textbooks

Types and Programming Languages by Benjamin Pierce
Formal Semantics of Programming Languages by Glynn Winskel