Learn Coq in Y Minutes

Re:Learn Coq in Y Minutes by kryptiskt on Tuesday November 26, 2019 @09:07AM (#21638343)

Software Foundations (https://softwarefoundations.cis.upenn.edu) is pretty informal and understandable, what it isn't is short. But it's a very useful resource.

The best general introduction is probably still Types and Programming Languages: (https://www.cis.upenn.edu/~bcpierce/tapl/index.html) It's a great book, but it doesn't get to dependent types.

[ Parent | on HN ]

Re:Learn Coq in Y Minutes by goodmattg on Tuesday November 26, 2019 @01:28PM (#21641133)

I'm currently in Prof. Pierce's class at UPenn! Can confirm this is a great book, and we literally work through the exercises. Taking this class AFTER using Scala in industry has really put a lot into context. It's so easy to start too - download CoqIDE or ProofGeneral and get to it!

[ Parent | on HN ]

Re:Learn Coq in Y Minutes by polymatter on Tuesday November 26, 2019 @11:44AM (#21639939)

I will second that Types and Programming languages is a great book. The next book, https://www.cis.upenn.edu/~bcpierce/attapl/index.html does get into Dependent Types.

[ Parent | on HN ]

Re:Learn Coq in Y Minutes by ouid on Tuesday November 26, 2019 @09:53AM (#21638709)

It should be mentioned that software foundations is basically a videogame that you can play in your coq interpreter. Short is less relevant than fun, imo.

[ Parent | on HN ]