about

Instructor:

Ben Delaware

bendy at purdue.edu

Office Hours: By Appointment

Course Description:

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
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.

resources

Course Text:

We will be using Software Foundations as the course textbook. Types and Programming Languages has a more in-depth treatment of semantics and type systems, while Certified Programming with Dependent Types is an excellent resource for applied programming and proving in Coq.

Coq:

The official project page of the Coq proof assistant has plenty of documentation. The latest version of Coq is 8.5, although Software Foundations will should work with the previous version, 8.4, as well.

policies

Grading:

Final grades will be assigned according to the following breakdown:

Homework Submission:

There will be bi-weekly assignments, requiring students to fill in missing definitions and proofs in an incomplete Coq file. Homeworks are to be submitted via email by 9PM on their assigned due 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. You receive two courtesy late days for the semester. Once you have used both those days, any late homeworks will not be accepted. While students can discuss assignments at a high-level, each student should produce the solutions they submit individually. A more detailed discussion of academic honesty can be found here.

schedule