30 citations · 99 across the 7 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
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.LO2011
Coquet: a Coq library for verifying hardware
Thomas Braibant
We propose a new library to model and verify hardware circuits in the Coq proof assistant. This library allows one to easily build circuits by following the usual pen-and-paper dia…
cs.LO2011★ 30 cited
Deciding Kleene Algebras in Coq
Thomas Braibant, Damien Pous
We present a reflexive tactic for deciding the equational theory of Kleene algebras in the Coq proof assistant. This tactic relies on a careful implementation of efficient finite a…