Formal Methods An Appetizer is excellent and has a companion site with toy formal methods implemented in F#: http://www.formalmethods.dk http://www.formalmethod

Formal Methods An Appetizer is excellent and has a companion site with toy formal methods implemented in F#: http://www.formalmethods.dk http://www.formalmethods.dk. However, it does not cover proof assistants. Alternatively you may enjoy these two. The latter is especially thorough, and begins with classical logic: * Concrete Semantics (Isabelle): http://concrete-semantics.org http://concrete-semantics.org * Program = Proof (Agda): https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...