CS565: Programming Languages
TTh 10:3011:45 
HAAS G066 

about
Instructor:
bendy at purdue.edu
Office Hours: Tuesday 3:004:30, LWSN 2116M
Teaching Assistant:
ye202 at purdue.edu
Office Hours: Thursday 2:003: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:

principles (e.g., semantics, type systems, specifications)

proof techniques and formal reasoning

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 indepth 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 Assignments 
40% 
Midterm (10/16) 
20% 
Final (12/14) 
30% 
Participation 
10% 
Homework Submission:
There will be biweekly 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 highlevel, each student should produce the
solutions they submit individually. A
more detailed discussion of academic honesty can
be found here.

(tentative) schedule


