Programming Languages

CMPS 203: Programming Languages


Nathan Whitehead
nwhitehe [at] ucsc [dot] edu
Baskin Engineering 259A
Office hours dedicated to CMPS 203: Tues 4-5 pm
General office hours: Tues 10-11 am, Thur 4-5 pm

Teaching Assistant

Jeremy Gottlieb
gottlieb [at] soe [dot] ucsc [dot] edu
Office hours: E2 316 Wed 1:30-2:30, also by email

Optional Textbooks

Types and Programming Languages, Benjamin Pierce

The Haskell School of Expression, Paul Hudak

The Formal Semantics of Programming Languages, Glynn Winskel

Interactive Theorem Proving and Program Development, Yves Bertot and Pierre Castéran

Certified Programming with Dependent Types, Adam Chlipala [PDF available online]

Course Work and Grading

  • (10%) In-class participation
  • (50%) Homework (4 assignments, use eCommons)
  • (40%) Final project (20-40hrs work per person) (30% report, 10% presentation)


Timetables subject to change based on class feedback.

  • Lazy functional programming in Haskell (3 lectures)
  • Operational semantics (3 lectures)
  • Implementing interpreters in Haskell (3 lectures)
  • Theorem proving in Coq (3 lectures)
  • Program verification in Coq (3 lectures)
  • Verified interpreters (3 lectures)


See the project page.

Instructors and Assistants