A library of formalised undecidable problems in Coq

uds-psl.github.io

53 points·zaik··5 comments

Since there are no other comments here, I will post this link to the Software Foundations book [1] by Benjamin Pierce et al., which may be of interest to anyone who wants to learn Coq.

> The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

> The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant.

> The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity is helpful. A one-semester course can expect to cover Logical Foundations plus most of Programming Language Foundations or Verified Functional Algorithms, or selections from both.

[1] https://softwarefoundations.cis.upenn.edu/

This book is very good. Reading it online is fine, but I highly recommend the curious download it actually run it from your favorite editor

Definitely! Otherwise it’s hard to keep track of how each “proof instructions” are manipulating the goals. Definitely give coqide or proofgeneral a try !

By the way, the first chapter is a very good introduction to what formal proving is about !

Last but not least, for all those that are interested in looking into coq, it was very helpful to start learning the basics of Ocaml first (especially variant types) ;)

Reply on news.ycombinator.com