CS 442 | SCS | UW

Revised Aug 31, 2015

CS 442: Principles of Programming Languages

Watch a video introduction to this course on YouTube.

General description

This course examines foundational issues in contemporary programming languages, including abstraction mechanisms, operational semantics, type systems, and extensibility.

Logistics

Audience

  • Fourth year CS majors

Normally available

  • Winter

Related courses

  • Pre-requisites: CS 240; Computer Science students only

For official details, see the UW calendar.

Software/hardware used

  • Standard UNIX environment with open-source language interpreters and compilers

Typical reference(s)

  • B. Pierce, Types and Programming Languages, The MIT Press, 2002

Required preparation

At the start of the course, students should be able to

  • Write efficient, readable programs from scratch, in several programming languages, that manipulate standard data structures (e.g., lists, trees)
  • Reason about the correctness and efficiency of such programs
  • Prove theorems about discrete mathematical structures (e.g., functions, relations, the natural numbers) using standard techniques (e.g., contradiction, induction)

Learning objectives

At the end of the course, students should be able to

  • Write efficient, readable programs from scratch in several new programming languages
  • Define and implement (via interpreters written in these new programming languages) operational semantics for extensions of the lambda calculus distilling features from said languages
  • Define typing rules for these extensions compatible with the type systems provided by said languages and implement type checking and type inference algorithms based on these rules
  • State and prove relevant theorems (e.g., progress, preservation) about type systems

Typical syllabus

Untyped lambda calculus and dynamically-typed languages (9 hours)

  • Grammar and reduction rules
  • Binding, scope, and substitution
  • Reduction strategies (eager vs. lazy evaluation)
  • Confluence and normalization
  • Simulating common programming language features (Booleans, natural numbers, lists, recursion)
  • Programming languages based on untyped lambda calculus (e.g., Lisp, Scheme, Racket)
  • Techniques for efficient interpreters (environments, closures, stores)

Typed lambda calculus and statically-typed languages (9 hours)

  • Typing rules and type-checking algorithms
  • Strong normalization and its implications
  • Recovering expressibility through extensions
  • Progress and preservation theorems
  • Type inference algorithms
  • Programming languages based on typed lambda calculus (e.g. SML, OCaml, Haskell)

Polymorphism (9 hours)

  • Types of polymorphism
  • Parametric polymorphism and its use in ML
  • System F
  • Higher-kinded polymorphism and its use in Haskell

Other topics (9 hours)

Topics chosen by the instructor to extend and/or complement the above. Possible choices include, but are not limited to:
  • Metaprogramming (e.g., macros)
  • Non-standard flow of control (e.g., continuations)
  • Object-oriented programming
  • Logic programming
  • Recursive types
  • Existential types and modules
  • Dependent types and certified programming