Programming Languages

CMPS 203: Programming Languages

Instructor

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)

Syllabus

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)

 Project

See the project page.