Skip to main content


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

Name Position Email Phone Office/consulting hours
Andrew Myers Instructor 255-8597 Upson 4133, Monday 11-12, Thursday 11-12
Shrutarshi Basu PhD TA [TBA] Upson 360, 1:30–3PM

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.