I joined Google Munich to work on the V8 Javascript compiler. Before, I worked on support for syntactic proofs with parallel de Bruijn indices in the Coq proof assistent. This results in the Coq library Autosubst.
