manik1337/csclub-coq-course-spring-2021

A course on formal verification at https://compsciclub.ru, Spring term 2021

Introduction to Formal Verification course at CS Club

Building HTML files locally

• Setup Alectryon using its installation instructions and add it to your PATH.
• Run make or make doc in the project root directory.

Class 1

• Intro to formal verification slides
• Intro to functional programming in Coq: source, rendered

Class 2

• Polymorphic functions & Dependent functions, Implicit Arguments, Notations, Product types and sum types: source, rendered

Class 3

• Defining logic, equality. Dependent pattern matching: source, rendered

Class 4

• Injectivity and disjointness of constructors, large elimination. Convoy pattern. Proofs by induction. Prop vs Type: source, rendered