The Coq mailing list

[Kumar Neeraj Verma <verma AT in.tum.de>]

Hi,

Nestor Catano schrieb:

> Hi,
>
> Does anyone know of work on modelling BDDs (Binary Decision Diagrams) or
> MDDs(Multivalued Decision Diagrams) in Coq or in any other
> proof-assistant/prover ?

See the BDDS contribution http://coq.inria.fr/contribs/bdds.html which 
provides
BDD algorithms which can be run inside Coq, as well as proofs. The SMC 
development
http://coq.inria.fr/contribs/smc.html extends this by providing garbage 
collection and
model checking.

Another development is BDD http://coq.inria.fr/contribs/bdd.html which 
models BDDs as trees,
without sharing. Its goal is to show that BDDs of equivalent formulae 
are identical.

Regards,
Kumar Neeraj Verma