Travelled to:1 × China
1 × Denmark
1 × India
1 × Italy
1 × United Kingdom
4 × USA
Collaborated with:G.Barthe A.Roth M.Gaboardi A.Albarghouthi P.Strub E.J.G.Arias T.Espitau B.Grégoire J.Ullman T.Roughgarden A.A.d.Amorim Z.S.Wu S.Weirich R.A.Eisenberg S.Khanna C.Smith Kevin Liao S.Smolka N.Foster D.Kozen A.S.0001 L.M.F.Fioriti Z.Huang A.Haeberlen A.Narayan B.C.Pierce S.Katsumata Ikram Cherigui M.Ying Nengkun Yu L.Zhou T.Sato A.A.0001 D.G.0001 T.Kappé Praveen Kumar 0003 David M. Kahn
Talks about:program (8) probabilist (7) privat (5) differenti (4) privaci (4) linear (4) proof (4) verif (3) coupl (3) type (3)
Person: Justin Hsu
DBLP: Hsu:Justin
Contributed to:
2015
2014
2014
2014
2014
2013201320132012
2018
2016201820172018
201920192020Wrote 22 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.
- ICALP-v1-2014-HsuRRU #linear #source code
- Privately Solving Linear Programs (JH, AR, TR, JU), pp. 612–624.
- ICML-c2-2014-GaboardiAHRW #query
- Dual Query: Practical Private Query Release for High Dimensional Data (MG, EJGA, JH, AR, ZSW), pp. 1170–1178.
- IFL-2014-AmorimGAH #linear #type checking
- Really Natural Linear Indexed Type Checking (AAdA, MG, EJGA, JH), p. 5.
- STOC-2014-HsuHRRW
- Private matchings and allocations (JH, ZH, AR, TR, ZSW), pp. 21–30.
- ICFP-2013-WeirichHE #similarity
- System FC with explicit kind equality (SW, JH, RAE), pp. 275–286.
- POPL-2013-GaboardiHHNP #dependent type #difference #linear #privacy
- Linear dependent types for differential privacy (MG, AH, JH, AN, BCP), pp. 357–370.
- STOC-2013-HsuRU #difference #equilibrium #privacy
- Differential privacy for the analyst via private equilibrium computation (JH, AR, JU), pp. 341–350.
- ICALP-v1-2012-HsuKR #distributed
- Distributed Private Heavy Hitters (JH, SK, AR), pp. 461–472.
- ESOP-2018-BartheEGGHS #logic #probability #source code
- An Assertion-Based Program Logic for Probabilistic Programs (GB, TE, MG, BG, JH, PYS), pp. 117–144.
- CAV-2016-BartheEFH #composition #invariant #probability
- Synthesizing Probabilistic Invariants via Doob's Decomposition (GB, TE, LMFF, JH), pp. 43–61.
- CAV-2018-AlbarghouthiH #constraints #proving #synthesis
- Constraint-Based Synthesis of Coupling Proofs (AA, JH), pp. 327–346.
- POPL-2017-AmorimGHKC #metric #semantics
- A semantic account of metric preservation (AAdA, MG, JH, SyK, IC), pp. 545–556.
- POPL-2017-BartheGHS #probability #proving #source code
- Coupling proofs are probabilistic product programs (GB, BG, JH, PYS), pp. 161–174.
- POPL-2018-AlbarghouthiH #difference #privacy #proving
- Synthesizing coupling proofs of differential privacy (AA, JH), p. 30.
- POPL-2018-BartheEGHS #probability #proving #source code
- Proving expected sensitivity of probabilistic programs (GB, TE, BG, JH, PYS), p. 29.
- PLDI-2019-SmolkaKKFHK0 #network #probability #scalability #verification
- Scalable verification of probabilistic networks (SS, PK0, DMK, NF, JH, DK, AS0), pp. 190–203.
- POPL-2019-SatoABGGH #approximate #convergence #higher-order #optimisation #probability #reasoning #source code #verification
- Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization (TS, AA0, GB, MG, DG0, JH), p. 30.
- POPL-2019-SmithHA #abstraction #probability
- Trace abstraction modulo probability (CS, JH, AA), p. 31.
- POPL-2020-BartheHL #logic #probability
- A probabilistic separation logic (GB, JH, KL), p. 30.
- POPL-2020-BartheHYYZ #proving #quantum #relational #source code
- Relational proofs for quantum programs (GB, JH, MY, NY, LZ), p. 29.
- POPL-2020-SmolkaFHKKS #algebra #linear #source code #testing #verification
- Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time (SS, NF, JH, TK, DK, AS0), p. 28.