16 citations · 16 across the 2 of their papers we have counts for
3 papers
cs.PL2016
Sparsity Preserving Algorithms for Octagons
Jacques-Henri Jourdan
Known algorithms for manipulating octagons do not preserve their sparsity, leading typically to quadratic or cubic time and space complexities even if no relation among variables i…
cs.LO2013★ 16 cited
Implementing and reasoning about hash-consed data structures in Coq
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
We report on four different approaches to implementing hash-consing in Coq programs. The use cases include execution inside Coq, or execution of the extracted OCaml code. We explor…
cs.PL2013
Implementing hash-consed structures in Coq
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases includ…