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.
  • Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant.
  • 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.
  • Some of my developments can be found on my github profile.

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