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.
  • 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.