Under construction

Announcements

  • Final grades have been released. Have a great summer!
  • Each student in this course is expected to abide by the Cornell University Code of Academic Integrity. Any work submitted by a student in this course for academic credit must be the student’s own work.
  • These web pages are still under development.

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.