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.