CS6501, Fall 2026

• Instructor: Kevin Sullivan · sullivan@virginia.edu
• Department: Computer Science, University of Virginia
• Meetings: Mondays & Wednesdays, 11:00 AM – 12:15 PM · Rice 508 — 28 sessions
• Office hours: Tuesdays, 1:00 – 3:00 PM · Rice 508
• Course book (living): https://kevinsullivan.github.io/Lean4CS1 · source: https://github.com/kevinsullivan/Lean4CS1

This syllabus is subject to change. Any such changes will be pre-announced and documented here.

About This Course

Software development is being transformed by AI in at least two big ways. First, AI is automating the production of a great deal of imperative code. Second, combined with the breakout success of proof assistants for formalization of abstract mathematical statements and proofs, AI promises far greater practicality and utility of formal specification and proof construction in routine industrial software production.

As of Fall 2026 there is exploding interest in the use of Lean for both formal mathematics and formal software specification and verification. A snapshot of where that stood at the start of this semester is in the appendix, Lean 4 beyond research.

However big challenges remain. Even with formal and machine-checked specifications, the rate at which generative AIs can produce specifications and proofs, now mixed together with ordinary programming types and functions and effects, means that one’s constructions can easily escape one’s intellectual control, even when it’s all formalized and proven.

The problem with loss of intellectual control is that it’s antithetical to good faith acceptance of accountability for harmful failures that were, or could and should have been, foreseen and averted. The social equation is you-are-accountable implies you-are-less-likely-to-fail implies I-can-trust-you-more and act accordingly. That trust is what a user pays for: assurances that the product is fit for use in all agreed respects, and the freedom to ignore the complexity behind them because someone else has taken care of it. The same reasoning underpins a legal system in which real people are punished. (At least that’s the theory.) And trust of that kind is crucial to the success of a system and of the society around it.

This course will emphasize the development of formal specification architectures as a vital practice for both guiding generative AIs to produce useful results and to maintain the intellectual control necessary for human beings to be held accountable for the harmful failures their systems produce.

Durable intellectual control depends on abstract software specification and proofs rooted in the generalized mathematics of the application domain, stating that theory precisely, and certifying separate computable implementations against it. It is also required for the sustained quality of evolving, long-lived software systems.

What formal methods give the developer is justified confidence that they can actually uphold the assurances their users are paying for and then relying upon. That confidence rests on two distinct objects of trust: the validity of the statements of the formal theory itself and verification of the proof certificates that connect implementation to the abstract theories they are required to implement in some form. Lean 4 provides a practical language in which theories, implementations, and proofs can coexist, but it does not eliminate either obligation: one must understand the mathematics being formalized, and one must understand the trusted proof-checking base on which that confidence depends.

This is a course for graduate students in computer science. The course has two main threads: learning to think and express concepts formally in Lean 4, and learning deep and abiding principles of intellectual control over software through readings of seminal papers leading up to the present moment.

Mathematical Thread: Two Parts

The mathematical thread in this course is in two parts.

• Part I — Certified Computation (the FP book). A functional-programming foundation, taught through the Curry–Howard correspondence, in which specifications are types. Students learn to read and write specifications as types, to derive terms that inhabit them, and to check their claims with the compiler. Part I does not assess proof construction. The proofs it contains are provided for students to read.
• Part II — Proof Construction. Part II builds on the Part I foundations and asks students to produce proofs of their own. The objects of study carry over (data, specifications, recursion, higher-order functions, sets, relations, type classes), reoriented from Type to Prop. Part II follows the discipline general theory → separate computable realization → certified bridge, and works toward the endpoint the semester is designed around: institutions and the satisfaction condition.

Lean is used from Week 1 onward. Part II changes the kind of work students do in Lean; it does not introduce Lean.

Schedule (Fall 2026 · Mondays & Wednesdays)

Two tracks run in parallel and are scheduled independently. Paper readings (Line I) keep their weekly cadence: one theme per paper-week, with full bibliographic references and PDF links given in each paper cell. A set is due at the session where it is listed and, where a ↳ (cont.) cell appears, carries into that week’s second session. The exception is Week 2, which carries two sets: set 1 due Wed Sep 2 and set 2 due Mon Sep 7. The Part I book track is compressed to two chapters per class session (one each on Wed Sep 16 and Mon Sep 28), run in order, beginning Wed Sep 2; once the book is complete (Mon Sep 28) the class proceeds to Part II (Lean programming and proof construction). Class does not meet Mon Oct 5 (fall reading days) or Wed Nov 25 (Thanksgiving); Labor Day (Mon Sep 7) meets. 28 sessions total.

‡ Part II topics (sessions 11–28) are tentative. The per-topic pacing (≈3 sessions each) is provisional. Part II keeps the discipline general theory → separate computable realization → certified bridge.

Grading

Course grades will be based on two components, weighted equally.

Participation means demonstrated preparation for and participation in class, including attendance and active participation in discussions. You have two “just out” days for the semester: two class meetings you may miss for any reason, with no explanation needed and no cost to your grade. Beyond those, habitual absences or inattention will result in losses against full credit, assessed periodically by the instructor. If you have special circumstances, talk with the instructor to reach a common understanding.

The competencies above describe what the work is assessed against. Weekly exercise sets are machine-checked for immediate feedback and count as preparation for class.

Course Materials in This Book

The Part I book track above draws on the CS1 Full Course chapters listed here. Part II builds new theory on top of these chapters. It introduces no further book chapters.

Unit 1 — Expressions, Functions, Recursion

• Week 0: Algebraic Types — Computation and Logic
• Week 1: Expressions, Types, and Values
• Week 2: Functions and Specifications
• Week 3: Recursion and Termination

Unit 2 — Algebraic Datatypes, Lists, Trees, Decidability

• Week 4: Algebraic Datatypes
• Week 5: Lists
• Week 6: Trees and BST Invariants
• Week 7: Polymorphism and Decidability

Unit 3 — Higher-Order Functions, Specifications

• Week 8: Higher-Order Functions
• Week 9: Specifications in Practice

Unit 4 — Sets and Relations

• Week 10: Sets and Relations

Unit 5 — Abstract Types, Type Classes

• Week 11: Abstract Types
• Week 12: Type Classes and Decidability

Unit 6 — Curry-Howard

• Week 14: The Curry-Howard Correspondence