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

This file was generated by bibtex2html 1.95.