CSEP 505: Programming Languages

Winter 2015

Course Overview

This course will offer an introduction to programming language semantics through implementation and formal models. It will emphasize functional programming and cover the key features of modern functional languages (including type systems and memory management), along with some ideas from object-oriented and other programming styles.

Lecture: Thursday, 6:30–9:20 pm, CSE 305 and MSR 99/1915 (distance). Archives
Office Hours: by appointment, CSE 342

Course Staff

Instructor: Greg Cooper (ghc[at]cs)
Greg received a Ph.D. in computer science from Brown University in 2008, advised by Shriram Krishnamurthi. In real life he works as a software engineer at Google.

TA: Eric Reed (ecreed[at]cs)

Course Tools

Discussion Board

Dropbox

Gradebook

Homeworks

Homework 1
Homework 2
Homework 3
Homework 4

Late Policy: Credit for late homework will be discounted by 10% per day for up to three days after the due date. After that, no credit will be given, unless arrangements were made in advance to accommodate an exceptional hardship.

Software

The course will use the Haskell programming language, which is freely available for recent versions of Windows, Mac OS, and Linux. The instructor uses haskell-mode for Emacs, but many other options are available for non-Emacs users.

Online Resources

haskell.org - the language's homepage (docs, extensive wiki)
Learn You a Haskell - a free, popular online guide to Haskell
Real World Haskell - a free online book about Haskell focusing on real applications
The Haskell wikibook - very complete (and of course it's free and online)

Approximate Schedule of Lecture Topics

  1. Course intro. Programming in Haskell. Syntax; parsing; evaluation.
  2. Variables; substitution; scope and environments. Functions. Evaluation strategies. (slides)
  3. Mutation. Monads. (slides)
  4. Untyped lambda calculus. Church encodings. Y-combinator. (slides)
  5. Continuations. (slides)
  6. Continuations, part 2; formal semantics (big-step). (slides)
  7. Small-step operational semantics. Simply-typed lambda calculus. (slides)
  8. Explicit parametric polymorphism (System F). Unification, Hindley-Milner type inference. Type soundness. (slides)
  9. Curry-Howard Correspondence. Recursive types. Subtyping. (slides)
  10. Something fun. (slides)