- Coquet: a Coq library for verifying hardware.
- Thomas Braibant. In Proc. 1st CPP, volume 7086 of
LNCS, pages 330-345. Springer, 2011.
- Tactics for reasoning modulo AC in Coq.
- Thomas Braibant and Damien Pous. In Proc. 1st CPP,
volume 7086 of
LNCS, pages 167-182. Springer, 2011.
- De Coquets Circuits.
- Thomas Braibant.
In Proc. JFLA 11, Studia Informatica Universalis, pages
93-116. Hermann, 2011.
- Rewriting modulo associativity and commutativity in Coq.
- Thomas Braibant and Damien Pous.
2nd Coq Workshop, July 2010.
- An efficient coq tactic for deciding Kleene algebras.
-
Thomas Braibant and Damien Pous.
In Proc. 1st ITP, volume 6172 of LNCS, pages
163-178.
Springer, 2010.
- A tactic for deciding Kleene algebras.
- Thomas Braibant and Damien Pous.
1st Coq Workshop, August 2009.
- The semantics of x86-cc multiprocessor machine code.
- Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli,
Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen,
and Jade Alglave. In POPL, pages 379-391. ACM,
2009.