Thomas Braibant

Publication Activity (10 Years)

Years Active: 2009-2014
Publications (10 Years): 0

Top Venues

CoRR

ITP

CAV

Log. Methods Comput. Sci.

Grenoble Alpes University, France (PHD)

Education History

Grenoble Alpes University, France

PHD

Publications

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

Thomas Braibant.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Thomas Braibant