CS565: Programming Languages
MWF 11:30-12:20 |
HAAS G-66 |
|
about
Instructor:
bendy at purdue.edu
Office Hours: Wednesday 3:00-4:30, LWSN 2116M
Teaching Assistant:
bsaberid at purdue.edu
Office Hours: Tuesday 4:00-5:30, HAAS 151
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.
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.5, but software foundations was designed
the previous version, which is still
availaible
here .
|
policies
Grading:
Final grades will be assigned according to the following breakdown:
Homework Assignments |
40% |
Midterm (Oct. 17) |
20% |
Final (TBA) |
30% |
Participation |
10% |
Homework Submission:
Homeworks are to be submitted via turnin
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
Date |
Topic |
Notes |
Homework |
08/22 |
Introduction |
Slides |
|
08/24 |
Crash Course on Coq |
Slides,
Basics.v |
|
08/26 |
Proof by Induction |
Slides,
Induction.v |
Homework 1
Due 9/02 |
08/29 |
Structured Data |
Slides,
Lists.v |
|
08/31 |
Polymorphism |
Poly.v |
|
09/02 |
More About Coq |
Slides,
Tactics.v |
Homework 2
Due 9/09 |
09/05 |
Labor Day (no class) |
|
|
09/07 |
Logic in Coq |
Slides
Logic.v |
|
09/09 |
Logic, Continuted |
Slides
Logic.v |
|
09/12 |
Propositions and Evidence |
IndProp.v |
|
09/14 |
Intro to Syntax and Semantics |
Slides
Imp.v |
Homework 3
Due 9/22
|
09/16 |
Denotational and Big-Step
Semantics |
Slides
|
|
09/19 |
Big-Step
Semantics in Coq |
Slides
Imp.v
|
|
09/21 |
Denotational Semantics
in Coq |
Slides
Denotational.v
|
|
09/23 |
Semantics Review
|
Slides
|
|
09/26 |
Axiomatic Semantics |
Slides
Hoare.v |
Homework 4
Due 10/03
|
09/28 |
Axiomatic Semantics,
Continued |
Slides
Hoare2.v |
|
09/30 |
Axiomatic Semantics,
Continued |
Slides
|
|
10/03 |
More Automation |
Auto.v
|
|
10/05 |
Introduction to
Small-Step Semantics |
Smallstep.v
Slides
|
|
10/07 |
Small-Step Semantics,
Continued |
|
Homework 5
Due 10/14 |
10/10 |
Fall Break (no class) |
|
|
10/12 |
Types
|
Types.v |
|
10/14 |
Types, Continued |
|
|
10/17 |
Midterm |
|
|
10/19 |
Simply Typed Lambda Calculus |
Stlc.v |
|
10/21 |
Simply Typed Lambda Calculus,
continued |
|
|
10/24 |
Progress, Preservation,
and Type Safety |
Types.v
Slides |
|
10/26 |
Progress, Preservation,
and Type Safety, Continued |
|
|
10/28 |
Progress, Preservation,
and Type Safety, Continued |
StlcProp.v
|
Homework 6
Due 11/5 |
10/31 |
Extensions to STLC |
MoreStlc.v |
|
11/02 |
Extensions to STLC |
|
|
11/04 |
Extensions to STLC in Coq |
|
|
11/07 |
Normalization of STLC |
Norm.v |
Homework 7
Due 11/16 |
11/09 |
Normalization, Continued |
|
|
11/11 |
Polymorphic Lambda Calculus |
|
|
11/14 |
Polymorphic Lambda Calculus, Continued |
|
|
11/16 |
Curry Howard Isomorphism |
ProofObjects.v |
|
11/18 |
Abstract Data Types and
Existential Types |
|
|
11/21 |
Abstract Data Types and
Existential Types Continued |
|
|
11/23 |
Thanksgiving Break (no class) |
|
|
11/25 |
Thanksgiving Break (no class) |
|
|
11/28 |
Parametricity |
|
|
11/30 |
Parametricity |
|
Homework 8
Due 12/7
|
12/01 |
Midwest PL Summit (no class) |
|
|
12/05 |
|
|
|
12/07 |
|
|
|
12/09 |
Wrapup and Final Review |
|
|
|
|
|