CS 565: Programming Languages

                                                                       August 22, 2017

Prof. Suresh Jagannathan
Room 3154J
Lawson Computer Science Building
Ph: x4-0971


Office Hours:

Tu, Th. 4 - 5PM


This course will examine the design and implementation of programming languages from a semantics-based perspective.  Our goal will be to develop tools that will enable us to both design and specify new language features, formally understand the implications of such designs, explain the rationale for existing features in modern languages, and develop mechanisms that allow us to prove interesting properties of langauge implementations. .  The course consists of three broad components: (1) principles (e.g., semantics, type systems, specifications); (2) proof techniques and formal reasoning and (3) mechanized 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 leverage proof techniques such as induction expressed using Coq, a powerful theorem prover and mechanized proof assistant.

A detailed syllabus can be found here.


All assignments and course lectures will use Coq. You will need to download version 8.5, 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.

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 being discussed by reviewing the corresponding source code and proofs.


August 22, 2017 August 24, 2017