Email Gateway (Aug 22 2022 at 13:13): Email Gateway (Aug 22 2022 at 13:13):From: Lawrence Paulson <lp15@cam.ac.uk>
That’s right, two entries in one day! And this is a very elaborate development, including monadic-based code generation.
Larry
Algorithms for Reduced Ordered Binary Decision Diagrams
Julius Michaelis, Maximilian Haslbeck, Peter Lammich and Lars Hupel
We present a verified and executable implementation of ROBDDs in Isabelle/HOL. Our implementation relates pointer-based computation in the Heap monad to operations on an abstract definition of boolean functions. Internally, we implemented the if-then-else combinator in a recursive fashion, following the Shannon decomposition of the argument functions. The implementation mixes and adapts known techniques and is built with efficiency in mind.
http://www.isa-afp.org/entries/ROBDD.shtml
Last updated: Nov 21 2024 at 12:39 UTC