Awesome

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.