This will be a graduate level course introducing techniques for formal reasoning about programs and specifications.
These techniques are fundamental to ensure that programs are correct and reliable. Bugs and insecurities in software have a huge societal cost, but ensuring programs correctness and reliability in practice is difficult. To assist programmers with this task, researcher in programming languages and software engineering have developed tools based on formal logic. The rigor of formal logic is useful to provide a formal specification for the program behaviour and to check, assisted by a machine, that the program meets this formal specification.
To introduce students to formal reasoning about programs and the basic techniques behind it we will use the Coq proof assistant and we will follow the approach developed in the online book Software Foundations. The precise schedule of the different classes will appear below.
The course is offered as a 3 credits class. This will be a graduate level course where each student is required to submit weekly assignment. There will be a midterm and a final. Students will also be invited to engage on one project and to present the results at the end of the course. The project is optional. Discussion about all the aspects of the course will also take place on Piazza.
The grading will be based on assignments, participation in class, and midterm and final exam.
The final grade will be composed as:
Every week at the end of the class the instructor will give the assignment for the week. The assignments must be submitted by the following Thursday at 6pm. The modality for submitting the assignments will appear here. Students can work on assignments in groups of two people. The components of the group have to be communicated to the instructor before the first assignment is due and must remain a group for the duration of the entire course.
Projects can take different forms depending on the interest of each student and can be discussed directly with the instructor. Students interested in this option should communicate with the instructor before the end of the third class. Some examples of what would constitute a good project are: implementation and proof of correctness of a non-trivial algorithm, formalization of programming language meta-theory, etc.
| Date | Topic | Software Foundations | Assignment |
|---|---|---|---|
| 8/29 | Introduction to the course | ||
| 9/09 | Functional programming in Coq | Basics.v | |
| 9/16 | Proof by Induction | Induction.v | |
| 9/23 | Working with Structured Data | Lists.v | |
| 09/30 | Polymorphism and Higher-order Functions | Poly.v | |
| 10/07 | More basic tactics | Tactics.v | |
| 10/14 | Logic in coq | Logics.v | |
| 10/21 | Inductively Defined Propositions | IndProp.v | |
| 10/28 | Total and Partial Maps | Maps | |
| 11/04 | Simple Imperative Programs | Imp.v | |
| 11/11 | Program Equivalence | Equiv.v | |
| 11/18 | Hoare Logic (Part I) | Hoare1.v | |
| 11/25 | Fall Break - no class | ||
| 12/2 | Hoare Logic (Part II) | Hoare2.v | |
| 12/9 | Small Step Operational Semantics | Smallstep.v | |
| 12/16 | Final |