Pierre-Yves Strub (史都伯)
Researcher at
IMDEA Software Institute -
Madrid - Spain
Previously, 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 Jouannaud
TypiCal (ex. LogiCal) team
- INRIA Saclay - Ile de France
- Laboratoire d'Informatique de l'X
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)
- Architecture Distribuee (2011/12 - Polytech Univ. Orsay - S8)
- Système (2010/11 - Polytech Univ. Orsay - S6)
- Architecture Distribuée (2010/11 - Polytech Univ. Orsay - S8)