- Course: CS 4501-001 (16039); CS 6501-008 (20760)
- Instructor: Kevin Sullivan
- Place: Web-Based Course (Synchronous)
- Time: TuTh 11:00AM - 12:15PM
Overview. This combined advanced undergraduate and graduate course will introduce students to constructive logic and its uses for specification and verification of programming languages, in particular, and of software systems, more generally. These tools have proven to be valuable in the production of high assurance software-driven systems ranging from compilers that provably generate correct code, to microprocessors that provably have certain critical correctness properties, to drones that are provably immune to important classes of security attacks.
Prerequisites. The course is open to advanced undergraduates who have take at least one course in theoretical computer science (algorithms, theory of computing, or CS 2102 as taught by Sullivan).
Learning Objectives. Students who take this course will come to understand advanced functional programming, higher-order logic and interactive proof construction; and major applications of these ideas to programming language specification, the specification and verification of programs written in imperative languages, and to the formalization of mathematics. The course uses the Lean Prover as an interactive proof assistant and programming system.
Required Reading (TENTATIVE). Baanen, Bentkamp, Blanchette, Holzel, and Limperg, The Hitchhiker's Guide to Logical Verification, Standard Edition, published online, Oct 12, 2020.
Background Reading. M. Lipovaca, Learn You a Haskell for Great Good!, No Starch Press, 2011. Read through Chapter 6, Section 4, Lambdas.
Grading (TENTATIVE). Course grades will be based on four homework assignments; a semester project; and two exams.
Schedule (TENTATIVE). Roughly speaking we will cover one chapter each week. Here are the section and chapter assignments by date, along with dates reserved for reviews and exams.
| Date | Section | Chapter |
|---|---|---|
| Warmup | History, purpose, and nature of logic: Watch https://www.youtube.com/watch?v=wOQuW6QFdos&feature=youtu.be | |
| Feb 2 | Basics | 1. Definitions |
| Feb 4 | ||
| Feb 9 | 2. Backward Proofs (Top-down, type-guided, structured development) | |
| Feb 11 | ||
| Feb 16 | 3. Forward Proofs (Bottom-up development) | |
| Feb 18 | ||
| Feb 23 | 4. Functional-Logic Programming | |
| Feb 25 | ||
| Mar 1 | Functional Programming | 5. Inductive Predicates |
| Mar 3 | ||
| Mar 8 | 6. Monads | |
| Mar 10 | ||
| Mar 15 | 7. Meta-Programming | |
| Mar 17 | ||
| Mar 22 | REVIEW | |
| Mar 24 | EXAM | |
| Mar 29 | Programming Semantics | 8. Operational Semantics |
| Mar 31 | ||
| Apr 1 | 9. Hoare Logic | |
| Apr 6 | ||
| Apr 8 | 10. Denotational Semantics | |
| Apr 13 | ||
| Apr 15 | Mathematics | 11. Logical Foundations |
| Apr 20 | ||
| Apr 22 | 12. Basic Mathematical Structures | |
| Apr 27 | ||
| Apr 29 | 13. Real and Rational Numbers | |
| May 4 | ||
| May 6 | REVIEW | |
| May 15 | EXAM 9AM-12PM or Takehome TBD |