Since September 2015, I'm a research
group led by Prof. Paulo
Verissimo at the SnT in Luxembourg,
working among other things on the
verification of distributed systems
and on intuitionistic type theory.
SnT webpage for more
From January 2011 to July 2015, I was a postdoc and then a research associate in the
PRL group led by
Prof. Robert L. Constable, where I was using and working on
the foundations of the Nuprl proof
While I was there, we built the
which we used to specify,
synthesize, and verify distributed
protocols such as Paxos.
PER semantics in Coq.