Under construction

Announcements

  • Students who are not enrolled but are interested in joining the course should fill out this form: https://docs.google.com/forms/d/e/1FAIpQLSfkQgG40cwUsgBx8Dhx8vsZjQU4T-f81Qm_se5JgF8lq3mnwA/viewform?usp=header
  • Lecture will be held in Gates 114 and also accessible via Zoom. The Zoom link will be available on CMSX.
  • 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.