CS565: Programming Languages
MWF 11:3012:20 
HAAS G66 

about
Instructor:
bendy at purdue.edu
Office Hours: Wednesday 3:004:30, LWSN 2116M
Teaching Assistant:
bsaberid at purdue.edu
Office Hours: Tuesday 4:005: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 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.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 highlevel, 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 BigStep
Semantics 
Slides


09/19 
BigStep
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
SmallStep Semantics 
Smallstep.v
Slides


10/07 
SmallStep 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 




