palmskog

7 ms·

1. 1.▲
   Coq developers looking for community feedback, including on name change(sondages.inria.fr)

   3 points by palmskog 5y ago|0 comments
2. 2.▲
   Coq is a Lean Typechecker(coq.discourse.group)

   91 points by palmskog 7y ago|31 comments
3. 3.▲
   by palmskog 9y ago

   Design verification using TLA+ and Alloy is a completely different game than verification at the level of code as in Verdi. While there are plenty of studies saying design verification is good in general, I'm not aware of any studies s
4. 4.▲
   by palmskog 9y ago

   If you're looking for programs verified down to the machine code level, using C and the Verified Software Toolchain (VST) is one option. C programs are proven in the Hoare style (pre/postconditions) inside Coq, and then compiled u
5. 5.▲
   by palmskog 9y ago

   Some new developments of the framework in the last two years: - packaging via OPAM to separate framework code and system code - support for specifying and proving liveness properties - support for proving Abadi/Lamport style refinement