Pierre-yves Strub (史都伯)
Non-permanent researcher at
INRIA / Microsoft Joint Center
Secure Distributed Computations and their Proofs Project
Previously, postdoc at
Tsinghua University
- LIAMA
- Beijing.
INRIA - FORMES project
Previously, Ph.D. student under the supervision of
Jean-Pierre Jouanaud.
TypiCal (ex. LogiCal) team
- INRIA Saclay - Ile de France
- Laboratoire d'Informatique de l'X
Office:
INRIA Futurs
Parc Club Orsay Université, Bât I - ZAC des Vignes
2-4, rue Jacques Monod
91893 ORSAY Cedex
France
Phone: +33 (0)1 69 35 69 90
EMail: pierre-yves [at] strub.nu
Research
Software
- Coq Modulo Theories 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
-
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.3pl2) including mingw (gcc 4.5.2), ocaml (3.12.0), camlp5 (5.15), Ssreflect (1.3pl2), emacs (23.3), and ProofGeneral (4.1).
Teaching
- Système (2010/11 - Polytech Univ. Orsay - S6)
- Architecture Distribuée (2010/11 - Polytech Univ. Orsay - S8)