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