miniblog.

← Back to all posts
May 26, 2014 at 11:30
"both proving that mental poker is impossible, and then giving a protocol to do it securely"! http://t.co/yXBRLHY4Ox

Related Posts

Sep 19, 2017 at 20:42
Proving that two funcs are equivalent is undecidable in general. Still, this SO answer describes some amazing tools!
haskell - How to compare two functions for extensional equivalence, as in (λx.2*x) == (λx.x+x)? - Stack Overflow
haskell - How to compare two functions for extensional equivalence, as in (λx.2*x) == (λx.x+x)? - Stack Overflow
Jul 11, 2016 at 18:29
A remarkable paper just uploaded to arXiv: *proving* that refactoring tools don't break C code!
Renaming Global Variables in C Mechanically Proved Correct
Renaming Global Variables in C Mechanically Proved Correct
Most integrated development environments are shipped with refactoring tools. However, their refactoring operations are often known to be unreliable. As a consequence, developers have to test their code after applying an automatic refactoring. In this article, we consider a refactoring operation (renaming of global variables in C), and we prove that its core implementation preserves the set of possible behaviors of transformed programs. That proof of correctness relies on the operational semantics of C provided by CompCert C in Coq.
Mar 16, 2014 at 18:34
UltraViolet http://t.co/e02LiYLVDk has an interesting model of users proving they own a copy, then letting them stream from anywhere.