5 ms·
A library of formalised undecidable problems in Coq
- ramboenel 6y agosincerament me la suda
- ramboenel 6y agookk
- ramboenel 6y agookkk
- soldehierro 6y ago¿Qué es exactamente lo que pretendes hacer con esta cadena de comentarios?
- benrbray 6y agoSince 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/ https://softwarefoundations.cis.upenn.edu/
- legobmw99 6y agoThis book is very good. Reading it online is fine, but I highly recommend the curious download it actually run it from your favorite editor
- globuous 6y agoDefinitely! 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) ;)