CS565: Programming Languages
|
about
Instructor:
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:
-
principles (e.g., semantics, type systems, specifications)
-
proof techniques and formal reasoning
-
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 Assignments |
40% |
| Midterm (TBA) |
20% |
| Final (TBA) |
30% |
| Participation |
10% |
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
|
|
|