Jacob Salzberg (Oct 29 2022 at 15:48): Jacob Salzberg (Oct 29 2022 at 15:48):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 :-)
Jacob Salzberg (Oct 29 2022 at 15:51):Especially one that lays bare proof trees or tableaux, and includes answers to exercises, haha
Karl Palmskog (Oct 29 2022 at 18:51):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
Patrick Nicodemus (Nov 01 2022 at 13:46):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