CS565: Programming Languages

MWF 11:30-12:20 HAAS G-66

about

Instructor:

Ben Delaware

bendy at purdue.edu

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

Teaching Assistant:

Baharak Saberidokht

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:

  1. principles (e.g., semantics, type systems, specifications)
  2. proof techniques and formal reasoning
  3. 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