Pierre-Yves Strub (史都伯)

Office:
Instituto IMDEA Software - Office 348
Campus Montegancedo UPM
28223-Pozuelo de Alarcón, Madrid
Spain

Phone: +34 91-101-2202 (ext. 4148)

EMail: pierre-yves [at] strub.nu

Research

Software

• 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.

A Formalization of Elliptic Curves in Coq

Have a look at the dedicated page.

Publications

• Fully Abstract Compilation to JavaScript
  with C. Fournet, N. Swamy J. Chen, P.-É. Dagand, and B. Livshits
  Accepted to the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL 2013
• Self-certification: Bootstrapping certified typecheckers in F* with Coq
  with J. Chen, C. Fournet, and N. Swamy
  Accepted to the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL 2012
• Modular Code-Based Cryptographic Verification
  with C. Fournet and M. Kohlweiss
  Accepted to the 18th ACM Conference on Computer and Communications Security - CCS 2011
• F*: Secure Distributed Programming with Value-Dependent Types
  with N. Swamy, J. Chen, C. Fournet, K. Bhargavan, and J. Yang
  Accepted to the 16th ACM SIGPLAN International Conference on Functional Programming - ICFP 2011
• Coq MTU: a higher-order type theory with a predicative hierachy of universes parameterized by a decidable first-order theory
  with B. Barras, J.-P. Jouannaud and Q. Wang (王前)
  Accepted to the 26th Annual IEEE Symposium on Logic in Computer Science - LICS 2011
• Coq Modulo Theory - [bib]
  19th EACSL Annual Conference on Computer Science and Logic - CSL 2010
• Coq Modulo Theory - Short Paper - with Qian Wang
  Short Presentation - 25th Annual IEEE Symposium on Logic In Computer Science - LICS 2010
• Type Theory and Decision Procedures
  Ph.D. Thesis
• From Formal Proofs to Mathematical Proofs: A safe, incremental way for building in first-order decision procedures - [bib]
  5th IFIP International Conference on Theoretical Computer Science - TCS 2008
  with F. Blanqui and J.-P. Jouannaud
• Building Decision Procedures in the Calculus of Inductive Constructions - [bib]
  16th EACSL Annual Conference on Computer Science and Logic - CSL 2007
  with F. Blanqui and J.-P. Jouannaud

Coq Bundle

Coq Bundle is a Windows installer for the Coq proof assistant (8.4pl1) including mingw (gcc 4.7.2), ocaml (4.00.1), camlp5 (6.07), ssreflect (1.4), emacs (24.2), ProofGeneral (4.2), and Tuareg O'Caml Mode (2.0.5).

Download Coq Bundle (8.4.1.3) - (Certificate Authority of the signing certificate)

You can also get a a 64bit version of the Coq Bundle. This last comes will a full 64bit OCaml toolchain (MinGW64 / OCaml64).

Teaching

• Système (2011/12 - Polytech Univ. Orsay - S6)
  • sujet du projet (29 mai 2012)
  • source de la bibliotheque (0.4)
  • planning soutenances groupe 2
  • correction
• Architecture Distribuee (2011/12 - Polytech Univ. Orsay - S8)
  • Notes de cours
  • Exemples du cours - Cette archive evoluera en fonction de l'avancement du cours.
  • TD 1 - La correction fait maintenant partie des exemples du cours (sous le non nu.strub.myrmi)
  • TD 2 - Bibliothèque de raytracing
    La correction fait maintenant partie des exemples du cours (sous le non nu.strub.rt.rmi)
• Système (2010/11 - Polytech Univ. Orsay - S6)
  • sujet du projet
• Architecture Distribuée (2010/11 - Polytech Univ. Orsay - S8)