View Code? Open in Web Editor
NEW
This project forked from anton-trunov/csclub-coq-course-spring-2021
A course on formal verification at https://compsciclub.ru/en, Spring term 2021
Coq 8.43%
HTML 65.28%
CSS 7.44%
JavaScript 16.05%
Makefile 0.02%
SCSS 2.78%
csclub-coq-course-spring-2021's Introduction
Introduction to Formal Verification course at CS Club
Building HTML files locally
- Setup Alectryon using its installation instructions and add it to your
PATH
. (You need Alectryon v1.1 or newer).
- Run
make
or make doc
in the project root directory.
- Polymorphic functions & Dependent functions, Implicit Arguments, Notations, Product types and sum types: source, rendered
- Seminar: seminar01.v
- Homework: hw02.v
- Injectivity and disjointness of constructors, large elimination. Convoy pattern. Proofs by induction.
Prop
vs Type
: source, rendered
- Seminar: seminar03.v
- Homework: hw04.v
- Verification of insertion sort and merge sort. Non-structurally recursive functions. Nested
fix
pattern. Program
plugin. Acc
-predicate. source, rendered
- Seminar: seminar08.v
- Homework: hw09.v
- A potpourri of tools: automation (linear integer arithmetic, hammers), Equations plugin, property based randomized testing, mutation proving, extraction source, rendered
- Seminar: seminar09.v
- Homework: no homework
Awesome exercise solutions by class participants
csclub-coq-course-spring-2021's People
Contributors