View the Project on GitHub TiarkRompf/cs565

Programming Languages

Spring 2016, 3 credits. Instructor: Tiark Rompf. TA: Grégory Essertel.

Links to Piazza and Blackboard

Lectures are Monday, Wednesday, Friday 8:30am to 9:20am Felix Haas Hall G066.

About the Course

This course will examine the design and implementation of programming languages from a foundational perspective.  Our goal will be to develop tools that will enable us to both design and specify new language features, to precisely understand the rationale for existing features in modern languages, and to understand how design decisions can impact implementations.  The course will be divided into roughly three parts: (1) principles (e.g., semantics, type systems, specifications); (2) proof techniques and formal reasoning and (3) automated theorem proving using the Coq proof assistant.   Our discussion of principles will be crafted in the context of definitions and theorems that capture salient properties of modern languages. The validation of these theorems will be undertaken using Coq, a powerful theorem prover and mechanized proof assistant.

A detailed syllabus can be found here (note: this document is from last year). For general policies about academic integrity etc. please see here.


All assignments and course lectures will take place using the mechanized proof assistant, Coq. You will need to download version 8.4, as well as an editor to facilitate writing interactive proofs. Proof General (which works with Emacs) and CoqIde, a standalone graphical editor are both good choices. On MacOS, Emacs, Coq and ProofGeneral are all easily installed using homebrew.

Course Text

The course text is Software Foundations. We will follow the material in the text closely. Each lecture will cover the material in the chapter by reviewing the corresponding source code and proofs.


We're following the blue path here


Your job is to complete all 1 and 2 star exercises in the given Coq file, except those marked as optional. Completing 3 star exercises or those marked optional is not required, but will improve your understanding, and can compensate for errors in other exercises.

Completed Coq files need to be submitted via Blackboard before midnight on the given date. Make sure that Coq accepts your file in its entirety. If it does not, it will not be graded. You can use Admitted to force Coq to accept incomplete proofs.

Basics.v: due on Fri, Jan 22
Induction.v: due on Sun, Jan 31
Lists.v: due on Sun, Jan 31
Poly.v: due on Sun, Feb 07
MoreCoq.v: due on Wed, Feb 17
Logic.v: due on Wed, Feb 17
Prop.v: due on Wed, Feb 24
MoreLogic.v: due on Wed, Feb 24
Imp.v: due on Wed, Mar 2
Equiv.v: due on Sun, Mar 6
Hoare.v: due on Sun, Mar 27
Hoare2.v: due on Sun, Mar 27
Smallstep.v: due on Sun, Mar 27
NOTE: Please read instructions on Blackboard for new submission format. Auto.v: (no exercises)
Types.v: due on Sun, April 3.
This time, homework includes exercise '3 stars (finish_progress)' and all of 'variation 1 ... 6'
Stlc.v: due on Sun, April 10.
StlcProp.v: due on Sun, April 17.
Homework includes all of 'variation 1 ... 7'
MoreStlc.v: due on Sun, April 24.
Homework onlyinclude the exercise STLC_extensions (4 stars).