“"Flocq" (Floats for Coq) is a formalization of #floating-point arithmetic for the #Coq proof assistant. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.” #formal-methods
on 02025-11-28#Coq is now #Rocq. #formal-methods
on 02025-11-28#Coq is based on a Calculus of Inductive Constructions which is really a #type-theory. #formal-methods
on 02025-08-06literate-programming #ebook developing the proof assistant "Proust" in Racket, apparently written for teaching Waterloo's Logic and Computation course, with an overview of propositional and predicate #logic, as well as #Coq and #Agda. #cc by-nc-sa
on 02021-02-09an #introduction to #formal-methods with #Coq
on 02017-11-25Adam Chlipala explains the basis of the Calculus of Inductive Constructions in this chapter of his #ebook on #Coq. #formal-methods
on 02017-07-13Adam Chlipala explains a bit about “library universes” in #Coq. #formal-methods #tutorial #toread
on 02016-08-02Benjamin Pierce’s #introduction to #Coq for #formal-methods, part of an #ebook on the subject. At least the beginning of this chapter seems pretty approachable, much more so than the stuff I’ve seen about ATS and whatnot.
on 02015-08-25The #formal-methods paper on #Coq for programming in #asm, "Coqasm".
on 02015-08-25Using #formalmethods (specifically #Coq and “Crash Hoare Logic”) to specify crash safety for #filesystems.
on 02015-08-23Using #Coq #formalmethods to do a proof of a sort program.
on 02015-08-14