Researcher at the IMDEA Software Institute - Madrid - Spain

Office: Instituto IMDEA Software - Office 348
Campus Montegancedo UPM
28223-Pozuelo de Alarcón, Madrid
Phone: +34 91-101-2202 (ext. 4148)
Email: pierre-yves [at]
See my DBLP page.
  • EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs.
  • Coq Modulo Theory is an extension of the Coq proof assistant embedding, in its computational mechanism, validity entailment for user-defined first-order equational theories.
  • All my Coq developments can be found on my github profile.