In this course, we learn the fundamentals of formal reasoning about programs using the Rocq proof assistant. We formally specify programming languages, that is, their syntax and operational semantics. We also formulate specifications of programs and prove that given programs satisfy their specification.
This course is based on the series Software Foundations.
