30 citations · 99 across the 7 of their papers we have counts for
7 papers
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…
MirrorShard: Proof by Computational Reflection with Verified Hints
Gregory Malecha, Adam Chlipala, Thomas Braibant +2
We describe a method for building composable and extensible verification procedures within the Coq proof assistant. Unlike traditional methods that rely on run-time generation and…
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…
Formal Verification of Hardware Synthesis
Thomas Braibant, Adam Chlipala
We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEatherweight SynthesIs). Fe-Si is a simplified version o…
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…
Tactics for Reasoning modulo AC in Coq
Thomas Braibant, Damien Pous
We present a set of tools for rewriting modulo associativity and commutativity (AC) in Coq, solving a long-standing practical problem. We use two building blocks: first, an extensi…
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…