4 ms·

Can you recommend and (1) books and (2) online lectures/courses on proofs which use Coq? Thanks!

• dougws 11y ago
  At this point, the standard intro text is Software Foundations [1]. I highly recommend it; it will teach you Coq and also probably make you a better programmer. After SF, Certified Programming with Dependent Types [2] gets more into the practice of proving serious programs correct. These books are both available online in the form of literate Coq files. As far as online lectures, OPLSS [3] often has Coq lectures which are quite good. [1] http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html [2] http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ [3] https://www.cs.uoregon.edu/research/summerschool/summer15/ https://www.cs.uoregon.edu/research/summerschool/summer15/
  • notsony 11y ago
    Thanks!
• deleted 11y ago
  [deleted]