Coq Workshop!

Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification.

We'll go through the "Basics" chapter of: "Software Foundations" a book about how to use Coq to prove things about computer science. https://softwarefoundations.cis.upenn.edu/lf-current/index.html

Install the latest version of the IDE from here: https://github.com/coq/coq/releases/tag/V8.8.1 and we'll work through the code together.

"Math people" may also be interested in this Meetup. If you know someone, please bring them along!

(Photo by John Moeses Bauan on Unsplash)