Travelled to:1 × Canada
1 × Czech Republic
1 × India
1 × Italy
1 × Japan
1 × Switzerland
2 × USA
Collaborated with:C.Fournet N.Swamy G.Barthe J.Hsu B.Grégoire J.Chen J.Jouannaud ∅ K.Bhargavan T.Espitau M.Gaboardi F.Blanqui S.Z.Béguelin B.Barras Q.Wang A.Rastogi E.J.G.Arias A.Roth P.Dagand B.Livshits J.Yang G.M.Bierman C.Hritcu C.Keller Antoine Delignat-Lavaud Simon Forest Markulf Kohlweiss Jean Karim Zinzindohoue
Talks about:program (5) type (5) probabilist (4) theori (3) order (3) javascript (2) higher (2) depend (2) secur (2) relat (2)
Person: Pierre-Yves Strub
DBLP: Strub:Pierre=Yves
Contributed to:
2015201420132012
2011
2011
20102007
2018201620172018Wrote 13 papers:
- POPL-2015-BartheGAHRS #approximate #design #difference #higher-order #privacy #refinement #relational
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy (GB, MG, EJGA, JH, AR, PYS), pp. 55–68.
- POPL-2014-BartheFGSSB #encryption #implementation #probability #relational #verification
- Probabilistic relational verification for cryptographic implementations (GB, CF, BG, PYS, NS, SZB), pp. 193–206.
- POPL-2014-SwamyFRBCSB #embedded #javascript #type system
- Gradual typing embedded securely in JavaScript (NS, CF, AR, KB, JC, PYS, GMB), pp. 425–438.
- POPL-2013-FournetSCDSL #compilation #javascript
- Fully abstract compilation to JavaScript (CF, NS, JC, PÉD, PYS, BL), pp. 371–384.
- POPL-2012-StrubSFC #coq #named #self
- Self-certification: bootstrapping certified typecheckers in F* with Coq (PYS, NS, CF, JC), pp. 571–584.
- ICFP-2011-SwamyCFSBY #dependent type #distributed #programming
- Secure distributed programming with value-dependent types (NS, JC, CF, PYS, KB, JY), pp. 266–278.
- LICS-2011-BarrasJSW #decidability #first-order #higher-order #named #type system
- CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory (BB, JPJ, PYS, QW), pp. 143–151.
- CSL-2010-Strub #coq #modulo theories
- Coq Modulo Theory (PYS), pp. 529–543.
- CSL-2007-BlanquiJS #calculus #induction
- Building Decision Procedures in the Calculus of Inductive Constructions (FB, JPJ, PYS), pp. 328–342.
- ESOP-2018-BartheEGGHS #logic #probability #source code
- An Assertion-Based Program Logic for Probabilistic Programs (GB, TE, MG, BG, JH, PYS), pp. 117–144.
- POPL-2016-SwamyHKRDFBFSKZ #dependent type #multi
- Dependent types and multi-monadic effects in F (NS, CH, CK, AR, ADL, SF, KB, CF, PYS, MK, JKZ, SZB), pp. 256–270.
- POPL-2017-BartheGHS #probability #proving #source code
- Coupling proofs are probabilistic product programs (GB, BG, JH, PYS), pp. 161–174.
- POPL-2018-BartheEGHS #probability #proving #source code
- Proving expected sensitivity of probabilistic programs (GB, TE, BG, JH, PYS), p. 29.