The semantics of x86-CC multiprocessor machine code. - Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli; Scott Owens; Tom Ridge; Thomas Braibant; Magnus O. Myreen; Jade Alglave (POPL, 2009)

An Efficient Coq Tactic for Deciding Kleene Algebras. - Thomas Braibant; Damien Pous (ITP, 2010)

Coquet: A Coq Library for Verifying Hardware. - Thomas Braibant (CPP, 2011)

Tactics for Reasoning Modulo AC in Coq. - Thomas Braibant; Damien Pous (CPP, 2011)

Deciding Kleene Algebras in Coq - Thomas Braibant; Damien Pous (Log. Methods Comput. Sci., 2012)

Algèbres de Kleene, réécriture modulo AC et circuits en coq. (Kleene algebra, Rewriting modulo AC and Circuits in Coq). - Thomas Braibant (2012)

Formal Verification of Hardware Synthesis. - Thomas Braibant; Adam Chlipala (CAV, 2013)

Implementing Hash-Consed Structures in Coq. - Thomas Braibant; Jacques-Henri Jourdan; David Monniaux (ITP, 2013)

MirrorShard: Proof by Computational Reflection with Verified Hints - Gregory Malecha; Adam Chlipala; Thomas Braibant; Patrick Hulin; Edward Z. Yang (CoRR, 2013)

Compositional Computational Reflection. - Gregory Malecha; Adam Chlipala; Thomas Braibant (ITP, 2014)

Implementing and Reasoning About Hash-consed Data Structures in Coq. - Thomas Braibant; Jacques-Henri Jourdan; David Monniaux (J. Autom. Reason., 2014)