Maître de conférences at École Polytechnique in the computer science department (DIX).

Member of the LIX (Laboratoire d'Informatique de l'X)

Office: École Polytechnique
Laboratoire d'informatique (LIX)
Bâtiment Alan Turing
1 rue Honoré d'Estienne d'Orves
CS35003 91120 Palaiseau Cedex, France
Phone: +33 1 77 57 80 29
Email: pierre-yves [at]
  • 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.

The following list of publications has been extracted from my DBLP page.