| τ | τ' |
|---|---|
| When | Tu/Th 1-2:15 |
| Where | CS 1263 |
| Who | Aws Albarghouthi |
| Office hours | Tue |
All notes and assignments wil be posted on this website.
Submission of assignments and course project deliverables is via Canvas.
Anonymous feedback can be submitted on this Google form
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.
The following will be populated as the course progresses:
-
Tue Welcome to the course / Intro to the beautiful lambda calculus
- notes
- Ch. 5 of TAPL
-
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
-
Tue Programming constructs in lambda calclus
- notes
- Ch. 5 of TAPL
-
Thu OCaml tutorial
-
Tue Fixpoints in lambda calculus
- notes (same as Tue)
- code from class
- Matt Might's blog: Y combinator in JS (See Might's other lambda calculus posts too.)
- See this nice blog post on deriving the Y combinator
-
Tue Introduction to types
- Ch. 8 of TAPL
-
Tue Simply typed lambda calculus
- Ch. 9 of TAPL
-
Thu Project meetings
you might also find helpful the notes from Sampson's Cornell class—this and this
-
Tue Type inference
- Ch. 22 of TAPL
-
Thu Types for an imperative language
- Ch. 3 of SPA (Ch. 2 has language definition)
you might also find helpful the notes from Sampson's Cornell class—this and this
-
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
-
Tue Propositional logic and SAT solvers
-
Thu First-order logic and SMT solvers
For more references, consult Bradley and Manna's book [CofC]—see references below
- Tue Bounded encodings
-
Tue Bounded encodings and Z3 solver
-
Thu Invariant generation with Horn clauses
-
Tue Invariant generation with predicate abstraction
-
Thu Lattice theory
- SPA ch. 4
-
Tue Lattice theory
- SPA ch. 4
-
Thu Abstract interpretation of programs
- SPA ch. 10
-
Tue Abstract interpretation of programs
- SPA ch. 10
-
Thu Numerical domains
- SPA ch. 6
-
Tue Termination
-
Thue project presentations
project presentations
Assignments will be posted here:
| Assignment | Due date |
|---|---|
| asn1 | Feb 15 |
| asn2 | Mar 14 |
| asn3 | April 15 |
| asn4 | Apr 30 |
Performance will be evaluated as follows:
| Task | X% |
|---|---|
| Research project | 45% |
| Assignments (4) | 40% |
| Project presentation | 10% |
| Class participation | 5% |
For the final project, you can work on a problem of your choice with a partner or by yourself.
-
Deliverable 1 (Feb 14) Send me a list of three project ideas.
-
5%: Deliverable 2 (Feb 25) 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 9) 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-15 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 7) 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 10-15 pages of Single-colum Latex article.
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
- [TAPL] Pierce, Types and Programming Languages. The MIT Press, 2002.
This is a free and excellent book that covers most material we cover in 704
- [FRAP] Chlipala Formal Reasoning About Programs
This is a fantastic (I think it's the best) book on static program analysis
- [SPA] Møller and Schwartzbach Static Program Analysis
This book talks about decision procedures and their applications in verification.
- [CofC] Bradley and Manna, The Calculus of Computation. Spring, 2007.
This is a short book on operational, axiomatic, and denotational semantics.
- [Sem] Nielson and Nielson Semantics with Applications. Springer, 2007.
The following book covers data-flow analysis and abstract interpretation.
- [PA] Nielson et al., Principles of Program Analysis Springer, 1999.
This is another abstract interpretation resource.
- [AI] Abramsky and Hankin, An Introduction to Abstract Interpretation.
There are multiple courses at other universities that overlap with the material we cover in CS704. Here are some that I found helpful: