Hi all,

Does anybody have pencil and paper Coq/CIC Course material/course material for Coq intended to be worked out in pencil and paper?

Thanks :-)

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: Oct 03 2023 at 02:34 UTC