Overview
Programming languages are a fundamental part of computer science. This course
introduces the formal tools needed to describe precisely what a program means.
These tools help us answer many useful questions about program analyses and
transformations, such as:
- Is this program correct?
- Will this program encounter a run-time type error?
- Is one program indistinguishable from another?
- Is this optimization a safe program transformation?
- Does this program compute the intended result? Does it leak information?
- Is this compiler translation correct?
- Can source language A be translated into target language B?
Topics include:
- Different styles of dynamic semantics, including operational, axiomatic,
and denotational semantics
- Static semantics, especially type systems
- Proofs by induction on derivations and structure
- A formal treatment of important programming language features such as
functions, laziness, exceptions, continuations, modules, type polymorphism, objects
and classes
Instructor: Andrew Myers
Course information
Course Staff
Recommended Texts
The following books are recommended but not required:
- Types and Programming Languages, by Benjamin Pierce
- The Formal Semantics of Programming Languages, by Glynn Winskel
These books are excellent sources for the course, so purchasing them is not a
bad idea. In a pinch, many students in the CS department will have this book,
and they will also be on reserve at the Engineering library.
Some other useful texts that provide a different perspective or more
depth in some areas are:
- Programming Languages: Theory and Practice, by Robert Harper
(online draft)
- Foundations for Programming Languages, by John Mitchell
- Semantics for Programming Languages, by Carl Gunter
- Basic Category Theory for Computer Scientists, by Benjamin Pierce
Some online resources for OCaml:
- Objective CAML Tutorial
- Introduction to the Objective Caml Programming Language, by Jason Hickey (online version)
- F#, a language similar to OCaml. You can use the Visual Studio IDE to write and debug F# programs.
- Comparison of SML and OCaml, by Andreas Rossberg.
- ledit, a tool to provide emacs-like editing (and history) to the OCaml toplevel. (Info on how to use ledit, and other tips for using the toplevel, here.)
For information about which readings are associated with each lecture,
see the course schedule.
Grading and submission policies
There will be 6 assignments, mostly written problems but some programming
problems in OCaml, totaling to 40% of your score. The first assignment
will be done solo; later ones will be done with a partner.
Assignment late penalties:
We are flexible about submitting assignments late. You will have 4 late days total during
the semester. No penalty will be applied if you limit the total number of late days to 4 or less.
Exams
There will be preliminary exam, time and location TBA.
The final exam is during the final exam period (location and time TBD) and will be 30% of your score.
Other components
We expect you to participate in class and elsewhere. 5% of the score will be
for participation (in-class, Piazza, course evals) and for in-class quizzes.
If you don't see a schedule for the course here, you are probably using
Internet Explorer, or else you have JavaScript turned off. If you have to use
another web browser, and apologies for the inconvenience.
Resources
Assignments
Other resources for programming assignments:
