Spring 2016, 3 credits. Instructor: Tiark Rompf. TA: Grégory Essertel.
Lectures are Monday, Wednesday, Friday 8:30am to 9:20am Felix Haas Hall G066.
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.
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.
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).