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] strub.nu
Software
  • 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.
Download
Publications

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