about

Instructor:

Ben Delaware

bendy at purdue.edu

Office Hours: Tuesday 3:00-4:30, LWSN 2116M

Teaching Assistant:

Qianchuan Ye

ye202 at purdue.edu

Office Hours: Thursday 2:00-3:30, HAAS 143

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

Discussion Forum:

The course piazza site will serve as the discussion board; all course announcements will also be posted there. In lieu of emailing the instructor or the TA with any general questions about using Coq or assignments, please post them to piazza so that any other students with the same question can see the answer.

Coq:

The official project page of the Coq proof assistant has plenty of documentation. The latest version of Coq is 8.8.1, which should be used for all assignments.

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

(tentative) schedule