The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

You might find our recent paper with Jacques-Henri Jourdan and David Monniaux about hash-consing in BDDs relevant to your situation.  The links to the code and a non-paywalled version of the paper are available here [1]. Specifically, we compare versions of BDD algorithms that are implemented using the straightforward state monad to other, smarter, implementations.   

Best,

Thomas

[1] http://braibant.github.io/update/2014/05/12/jar.html

Le 7 août 2014 19:28, "Dmitry Grebeniuk" <gdsfh1 AT gmail.com> a écrit :

Hello.

  I've asked this question in #coq irc, but with no practical success,
so I'm asking here.
  I want to prove an algorithm that involves mutable data structures
(namely, direct acyclic graph with mutable data associated with
vertices), some global mutable state, and recursion used to walk the
graph and modify vertex values.
  I can't use immutable data structures in my code: it would be
inconvenient for people who use my code, and it would be not
performance-wise.
  Also I don't need code extraction: manual porting of Coq code to
OCaml will be more or less straightforward.  I don't want to use Why,
because I want to understand every bit of my representation and
proofs.  (think it's a pedagogical purpose of this task.)
  A toy example of code I want to reason about:
https://gist.github.com/gdsfh/b5fc400f3e931e0194ad
  Here I want to prove that after calling "setmax somenode" all nodes
below "somenode" have "fld = max(n.fld)", where n are direct and
indirect children; and fld of leaf nodes is left intact.
  "State" monad is not very useful, since I have to prove things like
"eval (a := 1; a := 2) ==(after it..)==> eval(a) == 2", and state
monad won't ease proofs compared to explicit state passing.  (am I
wrong?)
  Which keywords, papers or pointers can you suggest?