Alex Shan

dblp:248/7758 · DBLP profile ↗
← Back
1ranked-venue papers
0as first author
0since 2021 · last 2019
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 1

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
1 paper
Programming languages and type systems · 100%
Network and information security
1 paper
Privacy and data protection · 100%

Topics — the 3 heaviest of 3, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Privacy and data protection
differential privacy
0.412019
Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy · Proc. ACM Program. Lang. 2019
Programming languages and type systems
higher-order languages
0.412019
Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy · Proc. ACM Program. Lang. 2019
Programming languages and type systems › type systems › substructural type systems
linear types
0.412019
Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy · Proc. ACM Program. Lang. 2019

Methods — techniques the papers use, named apart from their topics

type system design · 0.8privacy proofs · 0.4privacy proof · 0.4
YearPublicationVenuePosition
2019 Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy
abstract
During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by an expert in the field. Language-based techniques have been proposed for fully automating proofs of differential privacy via type system design, however these results have lagged behind advances in differentially-private algorithms, leaving a noticeable gap in programs which can be automatically verified while also providing state-of-the-art bounds on privacy. We propose Duet, an expressive higher-order language, linear type system and tool for automatically verifying differential privacy of general-purpose higher-order programs. In addition to general purpose programming, Duet supports encoding machine learning algorithms such as stochastic gradient descent, as well as common auxiliary data analysis tasks such as clipping, normalization and hyperparameter tuning - each of which are particularly challenging to encode in a statically verified differential privacy framework. We present a core design of the Duet language and linear type system, and complete key proofs about privacy for well-typed programs. We then show how to extend Duet to support realistic machine learning applications and recent variants of differential privacy which result in improved accuracy for many practical differentially private algorithms. Finally, we implement several differentially private machine learning algorithms in Duet which have never before been automatically verified by a language-based tool, and we present experimental results which demonstrate the benefits of Duet's language design in terms of accuracy of trained machine learning models.
Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang 0001, Neel Somani, Mu Zhang 0001, Alex Shan, Dawn Song
Proc. ACM Program. Lang.10