Stream: Coq users

Topic: Pencil and Paper Coq Course

view this post on Zulip 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 :-)

view this post on Zulip Jacob Salzberg (Oct 29 2022 at 15:51):

Especially one that lays bare proof trees or tableaux, and includes answers to exercises, haha

view this post on Zulip 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

view this post on Zulip 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: Oct 03 2023 at 02:34 UTC