Thomas Braibant
Personnal data
Office: 04 76 61 54 57
B116, INRIA Rhône-Alpes, 655, avenue de l'Europe, Montbonnot
38334 Saint Ismier
Home: 06 63 30 37 53
42 avenue Alsace Lorraine, 38000 Grenoble
Mail:
Thomas
dot Braibant
at gmail
dot com
PGP public key key
Situation
I am working as a PhD on the development of algebraic tools in proof
assistants that should make it possible, at some point, to study and
certify distributed systems. My supervisors are
Damien Pous and
Jean-Bernard Stefani in the team Sardes of the INRIA
Grenoble.
New: With Damien, we have just released an efficient
reflexive tactic for deciding Kleene algebras; we plan to pursue this
work by implementing other decision procedures. The current state of
the corresponding library (ATBR) can be found there:
ATBR.
New: With Damien, we released rewriting tactics
working modulo AC for Coq:
aac_tactics.
New: Coquet : a Coq library for verifying hardware.
Publications
See
here
Some talks
- An efficient tactic for deciding Kleene Algebras .pdf , ITP 2010
- Rewriting modulo associativity and commutativity in Coq .pdf , second coq workshop, 2010
- A tactic for deciding Kleene Algebras .pdf , first coq workshop,
august 2009
- A tactic for deciding Kleene Algebras .pdf , séminaire gallium, june 2009
- A tactic for deciding Kleene Algebras .pdf , LIX, april 2009
Past situation
I am a former student of the ENS Lyon, and
made my master internship under the supervision
of
Francesco Zappa
Nardelli and
Peter
Sewell
Some people