Does anybody have pencil and paper Coq/CIC Course material/course material for Coq intended to be worked out in pencil and paper?
Especially one that lays bare proof trees or tableaux, and includes answers to exercises, haha
Coq is a software implementation of a variant of CIC. You won't find much pen-and-paper material on Coq itself, but one often-recommended book on type theories with exercises is TAPL, and one book on logic/proofs/tableau with exercises is Logic in Computer Science
The book "Type Theory and Formal Proof" by Nederpelt and Geuvers is also primarily about the CoC.
Last updated: Feb 04 2023 at 21:02 UTC