From September 2015 to May 2019, I was 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.
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.