CS 704 course website - Principles of Programming Languages
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
asn
code
notes
README.md

README.md

CS 704: Principles of Programming Languages (Spring 2018)

τ τ'
When Tu/Th 230-345
Where CS 1325
Who Aws Albarghouthi
Office hours Tue 100-200 in CS 6363

All notes and assignments wil be posted on this website.

Submission of assignments and course project deliverables is via canvas.

Course description

This course covers a range of topics in programming languages, including lambda calculus and type theory, functional programming, logics for encoding programs, and automated verification techniques.

The goal is to expose students to a range of mathematical and practical tools for reasoning about programs.

Lectures

The following will be populated as the course progresses:

Week 1 (Jan 22) Lambda calculus

  • Tue Welcome to the course / Intro to the beautiful lambda calculus

  • Thu Computing with lambda calculus

    • notes
    • Chs. 5 and 6 of TAPL

you might also find helpful the notes from Sampson's Cornell class—this and this

Week 2 (Jan 29) Programming constructs & fixpoints in lambda calculus

Asn 1 out

Week 3 (Feb 5) The Church–Rosser theorem / FP

  • Tue Deep dive into functional programming

    • no notes—tonnes of online tutorials
  • Thu The Church–Rosser theorem

Deliverable 1 due

Week 4 (Feb 12) Types

  • Tue Introduction to types

    • Ch. 8 of TAPL
  • Thu Simply typed lambda calculus

    • Ch. 9 of TAPL

you might also find helpful the notes from Sampson's Cornell class—this and this

Asn 1 due / Asn 2 out

Week 5 (Feb 19) Type inference & polymorphism

  • Tue Type inference

    • Ch. 22 of TAPL
  • Thu System F cancelled due to baby

    • Ch. 23 of TAPL

you might also find helpful the notes from Sampson's Cornell class—this and this

Week 6 (Feb 26) Semantics

  • Tue Operational semantics

    • The class presentation is based on Nielsen and Nielsen's book [Sem] -- see their comprehensive slides here
  • Thu Axiomatic semantics

    • The class presentation is based on Nielsen and Nielsen's book [Sem] -- see their comprehensive slides here

you might also find helpful Chs 7 (operational semantics) and 12 (axiomatic semantics) of Chlipala's FRAP book, which is freely available

Week 7 (Mar 5) Logic & SAT/SMT

  • Tue Propositional logic and SAT solvers

    • The class presentation will follow Dillig's slides: here and here
  • Thu First-order logic and SMT solvers

    • The class presentation will follow Dillig's slides: here and here and here

For more references, consult Bradley and Manna's book [CofC]—see references below

Asn 2 due / Deliverable 2 due / Asn 3 out

Week 8 (Mar 12) Transition systems & program encodings

Week 9 (Mar 19) Automated verification

  • Tue Finding Hoare proofs with Horn clauses

  • Thu Automatically solving Horn clauses / intro to assignment 4

    • same notes as Tue
    • we will also cover k-induction, the subject of asn3, which is covered in Sec 8 of the notes from last week

Asn 3 due / Asn 4 out

Week 10 (Mar 26) SPRING BREAK

Week 11 (Apr 2) Automated verification continued

  • Tue Implementing a mini verifier

  • Thu Boolean abstraction and predicate refinement

Week 12 (Apr 9) Handling concurrency

  • Tue To understand concurrency proof rules, we begin with recurisve proofs

    • code
    • notes see section on recursion (more details to be added)
  • Thu Rely-Guarantee Proofs

Deliverable 3 due

🔥 Week 13 (Apr 16) Abstract Interpretation

  • Tue Intro to Abstract Interpretation

    • notes
    • More details in Ch. 4 of PA (see references). See also FRAP Ch. 7.
  • Thu Abstract interpretation of programs

    • same as above

Asn 4 due / Asn 5 released

Week 14 (Apr 23)

  • Tue Hyperproperties: non-interference and side-channel leakage

  • Class presentations will be held this week.

Week 15 (Apr 30)

  • Class presentations will be held this week.

Asn 5 due / Deliverable 5 is due May 11

Assignments

Assignments will be posted here:

Assignment Due date
asn1 Feb 15
asn2 Mar 1 Mar 8
asn3 Mar 22
asn4 Apr 17
asn5 May 3

Evaluation

Performance will be evaluated as follows:

Task X%
Research project 45%
Assignments (5) 40%
Project presentation 10%
Class participation 5%

Course Project

For the final project, you can work on a problem of your choice with a partner or by yourself.

  • Deliverable 1 (Feb 5) Send me a list of three project ideas.

  • 5%: Deliverable 2 (Feb 26) Submit a 2-3 page proposal including the following: The statement of the problem to be investigated An explanation of why the problem is interesting A description of what you propose to do. Explain the elements that you will have to build. Explain the elements that you can pick up from open-source sites. Explain the experiment(s) or performance measurement(s) that you plan to carry out. Two good approaches are State the hypothesis that you hope to refute. Complete the following sentence: "The experiments were designed to shed light on the following questions: . . ." Then explain what you plan to measure; how you will measure it (if it is not obvious); and where you will obtain test cases. List the tasks, broken down into two or three milestones

  • 5%: Deliverable 3 (Apr 12) Submit a description of progress, implementation plan with completed steps checked off, and experimentation plan. Please turn in an updated proposal (with changes marked with changebars, and your new material added as "Appendix B: Progress Report".

  • 10%: Deliverable 4 (last 2 weeks of class) 10-minute oral presentations (plus 5 minutes for questions/discussion) will be given during class. You will need to e-mail me an abstract (in plaintext) giving the title, project participants, and a two-paragraph to three-paragraph summary of what will be presented.

  • 35%: Deliverable 5 (May 11) Final writeup: The final writeup should be modeled after a typical conference paper. There is no length requirement or limit, but I would expect it to be somewhere around 6-10 pages of ACM's double-column conference formats.

Resources

There are no required textbooks for this class. The following is a list of books that should be useful references for different parts of the course.

This is an excellent reference for our lambda calculus and types material

This is a free and excellent book that covers most material we cover in 704

This book talks about decision procedures and their applications in verification.

This is a short book on operational, axiomatic, and denotational semantics.

The following book covers data-flow analysis and abstract interpretation.

This is another abstract interpretation resource.

There are multiple courses at other universities that overlap with the material we cover in CS704. Here are some that I found helpful: