Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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

[2] http://adam.chlipala.net/cpdt/

[3] https://www.cs.uoregon.edu/research/summerschool/summer15/



Thanks!




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: