Lectures on Software Foundations
By Michael Clarkson.
This repo contains materials to accompany a series of YouTube videos on the textbook Software Foundations, volume 1. The videos grew out CS 4160 Formal Verification, a course taught at Cornell University by Michael Clarkson. The textbook is a project led by Benjamin C. Pierce at the University of Pennsylvania. Clarkson is a contributing author.
-
Some Coq installation advice is available.
-
The notes directory contains the Coq source files used in the lecture videos. You can follow along with them yourself while watching.
-
An HTML version of the textbook is available. After watching the lectures on a chapter, you can read the full chapter.
-
The textbook directory contains the Coq source files for the full textbook chapters. You can download them to complete the textbook exercises yourself.