specialgoodness

7 ms·

1. 1.▲
   by specialgoodness 10mo ago

   The Nelson-Oppen simplifier is a great piece of work, but it is not the first SAT solver. Boyer and Moore published their formally verified SAT solver in their 1979 A Computational Logic, the first book on the Boyer-Moore Theorem Prover, t
2. 2.▲
   by specialgoodness 10mo ago

   As an insider and major user of this effort in ImandraX, I must say: Moonpool and OCaml5 concurrency have been an absolute game-changer! Awesome read.
3. 3.▲
   by specialgoodness 10mo ago

   Xavier Leroy as Lou Reed... :-) Don't forget the amazing theorem provers too, like Imandra ( https://www.imandra.ai/core ), HOL-Light ( https://hol-light.github.io/ ) and Rocq ( https://rocq
4. 4.▲
   by specialgoodness 1y ago

   check out Imandra's platform for neurosymbolic AI - https://www.imandra.ai/
5. 5.▲
   by specialgoodness 2y ago

   Beautiful! Imandra is a modern Boyer-Moore style theorem prover for higher-order functional programming (its logic is based on a typed higher-order subset of OCaml rather than Boyer-Moore's basis on an untyped first-order subset of Pur
6. 6.▲
   by specialgoodness 2y ago

   This is interesting work but it totally misses the boat when it talks about the current state of the art. They cite a 2014 version of the Goel-Hunt-et al formal x86 model in ACL2, but they fail to talk about its modern version. The modern v