Skip to main content





Announcements

  • Check Piazza for announcements.

Overview

This is a course on using proof assistants to build provably correct software: software accompanied by a formal proof of correctness. Normally, the word “proof“ means an informal English argument, but in this course, a proof is an explicit formal object constructed using a proof assistant. The proof assistant mechanically checks that each step in the proof is valid. Students learn to use the Coq proof assistant and use it to do a project in which the properties of some software system or language are formally modeled and proved. Students will also read and discuss papers related to certified software.

Instructors: Greg Morrisett and Andrew Myers

Course information

Course Staff

Placeholder for staff

Prerequisites

CS 6110 or permission of the instructor.

Coursework and Evaluation

Coursework will consist of problem sets, in-class exercises, reading topical research papers and discussing them in class, and a final project done with a partner.

Students will be evaluated based on class participation, assignments, and their final project.

Placeholder for schedule

Resources

The Coq Proof Assistant

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.

Coq Integrated Development Environment

The Coq Integrated Development Environment (coqide) is a graphical development environment for Coq. It allows the user to navigate within a Coq vernacular file, executing corresponding commands or undoing them respectively.

Proof General

An Emacs-based generic front-end for proof assistants.

Coq Survival Kit (Pichardie and Blazy)

Some nice slides showing what the most useful Coq tactics do.

Software Foundations (Pierce et al.)

Topics include basic concepts of logic, computer-assisted theorem proving, the Coq proof assistant, functional programming, operational semantics, Hoare logic, and static type systems. The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity will be helpful.

Verified Functional Algorithms (Appel)

Certified Programming with Dependent Types (Chlipala)

Formal Reasoning about Programs (Chlipala)

Other readings

Assignments