LINKS.org

Useful links

Course page at edu.tinkoff.ru (in Russian)

Video lectures (in Russian)

How to install Coq and Mathcomp

• https://github.com/coq/coq/wiki#coq-installation
• https://github.com/math-comp/math-comp/blob/master/INSTALL.md

IDE-like editors

• VsCoq (Visual Studio Code based)
• CoqIDE (see Coq’s installation instructions)
• Proof General (Emacs based)

Documentation

• The Coq Reference Manual

SSReflect/Mathcomp-related

• Books, lecture notes, cheatsheets, tutorials, reference manual, videos of talks
• Code Style Guide
• Search: tips, tricks, and gotchas
• Advanced use of rewrite tactic: A Language of Patterns for Subterm Selection - G. Gonthier, E. Tassi

Background reading

• Constructive Logic (lecture notes) by F. Pfenning(2008)
• The Devil of the Excluded Middle

Exercises

• Coq Math Problems: Interesting, challenging, or fun math problems formalized in Coq
• Exercises on Generalizing the Induction Hypothesis by J.R. Wilcox