Thomas Braibant

16 papers A* 2B 5Journal 8
YearRankTypeTitle / Venue / Authors
2014 B conf
Compositional Computational Reflection.
ITP
Gregory Malecha, Adam Chlipala, Thomas Braibant
2014 J jnl
Implementing and Reasoning About Hash-consed Data Structures in Coq.
J. Autom. Reason.
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013 J jnl
Formal Verification of Hardware Synthesis
CoRR
Thomas Braibant, Adam Chlipala
2013 A* conf
Formal Verification of Hardware Synthesis.
CAV
Thomas Braibant, Adam Chlipala
2013 B conf
Implementing Hash-Consed Structures in Coq.
ITP
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013 J jnl
Implementing and reasoning about hash-consed data structures in Coq.
CoRR
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013 J jnl
Implementing hash-consed structures in Coq
CoRR
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
2013 J jnl
MirrorShard: Proof by Computational Reflection with Verified Hints
CoRR
Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, Edward Z. Yang
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 J jnl
Deciding Kleene Algebras in Coq
Log. Methods Comput. Sci.
Thomas Braibant, Damien Pous
2011 B conf
Coquet: A Coq Library for Verifying Hardware.
CPP
Thomas Braibant
2011 J jnl
Coquet: a Coq library for verifying hardware
CoRR
Thomas Braibant
2011 B conf
Tactics for Reasoning Modulo AC in Coq.
CPP
Thomas Braibant, Damien Pous
2011 J jnl
Tactics for Reasoning modulo AC in Coq
CoRR
Thomas Braibant, Damien Pous
2010 B conf
An Efficient Coq Tactic for Deciding Kleene Algebras.
ITP
Thomas Braibant, Damien Pous
2009 A* conf
The semantics of x86-CC multiprocessor machine code.
POPL
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave