Higher-Order Approximate Relational Refinement Types
for Mechanism Design and Differential Privacy
Gilles Barthe‹
Marco Gaboardi;
Emilio Jesús Gallego Arias#
Justin Hsu#
Aaron Roth#
Pierre-Yves Strub‹
IMDEA Software Institute

;

University of Dundee, Scotland

#

University of Pennsylvania

tifact

eu

OPL *
* P se * Consi

at e d

arXiv:1407.6845v2 [cs.PL] 29 Oct 2014

* Easy to
ed
R
nt

Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory—Semantics; D.2.4 [Software Engineering]: Software/Program Verification.
Keywords program logics; probabilistic programming

1.

Introduction

When designing algorithms, we usually assume that the inputs
are correctly reported. However, in the real world, inputs may be
provided by people who may want to influence the outcome of
the algorithm. Mechanism design is the field of algorithm design
where the inputs to the algorithm (often called a mechanism) are
controlled by strategic agents who may manipulate what their
inputs. In this setting, it is not enough to design an algorithm which
behaves correctly on correct input; the design of the mechanism
Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. Copyrights for components of this work owned by others than the
author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or
republish, to post on servers or to redistribute to lists, requires prior specific permission
and/or a fee. Request permissions from permissions@acm.org.
POPL ’15, January 15–17, 2015, Mumbai, India.
Copyright is held by the owner/author(s). Publication rights licensed to ACM.
ACM 978-1-4503-3300-9/15/01. . . $15.00.
http://dx.doi.org/10.1145/10.1145/2676726.2677000

Ev

Mechanism design is the study of algorithm design where the inputs
to the algorithm are controlled by strategic agents, who must be
incentivized to faithfully report them. Unlike typical programmatic
properties, it is not sufficient for algorithms to merely satisfy the
property—incentive properties are only useful if the strategic agents
also believe this fact.
Verification is an attractive way to convince agents that the incentive properties actually hold, but mechanism design poses several
unique challenges: interesting properties can be sophisticated relational properties of probabilistic computations involving expected
values, and mechanisms may rely on other probabilistic properties,
like differential privacy, to achieve their goals.
We introduce a relational refinement type system, called
HOARe2 , for verifying mechanism design and differential privacy.
We show that HOARe2 is sound w.r.t. a denotational semantics,
and correctly models p, δq-differential privacy; moreover, we show
that it subsumes DFuzz, an existing linear dependent type system
for differential privacy. Finally, we develop an SMT-based implementation of HOARe2 and use it to verify challenging examples of
mechanism design, including auctions and aggregative games, and
new proposed examples from differential privacy.

ll Docum
We
e

Abstract

A EC *

st

* Complete

*

t
en

*

Ar

alu

‹

must convince (incentivize) agents to provide their correct inputs to
the algorithm.
The canonical application of mechanism design is auction design.
In an auction, the algorithmic problem can be very simple: for
instance, allocate some set of goods amongst a set of n agents so
as to maximize their sum value for the goods. The inputs to the
algorithmic problem are simply the agents’ values for the goods, but
these are unknown to the algorithm designer. Instead, the mechanism
must elicit bids. To incentivize agents to bid honestly, actions
compute a price that each agent must pay. Auctions are generally
designed so that the allocation and payment rules incentivize agents
to bid their true value for the goods, no matter what their opponents
do. An auction that satisfies this property is said to be dominant
strategy incentive compatible, or simply truthful. This is among the
most important solution concepts—predictions about behavior of
strategic agents—in mechanism design.
Beyond auctions, mechanisms design can be used to handle more
abstract games where agents have a variety of actions and a realvalued utility function based on the actions selected by all agents.
In most settings, agents do not have any dominant strategies, and
so we must be satisfied with weaker solution concepts like Nash
equilibria. Informally, a set of actions, one for each player, forms
a Nash equilibrium if no player can increase her utility unilaterally
deviating to a different action so long as no other player deviates.1
The hope is that strategic agents will collectively decide to play at
an equilibrium: no single agent can gain by deviating.
However, Nash equilibria can be an unrealistic prediction of
behavior. First of all, they are generally not unique: agents must
somehow coordinate to play at a single equilibrium, but different
agents might prefer different equilibrium outcomes. Second of all,
in games with a large number of players, agents generally do not
have complete knowledge about everyone’s utility functions, and
so may not even know what the Nash equilibria of the game are.
To help players coordinate on an equilibrium, one approach is to
design an equilibrium selection mechanism. Agents are asked to
report their utility functions to some mediator, and the mediator
suggests some action for them to play. Agents are strategic, so
they are free to misreport their utility function, or disregard the
mediator’s suggestion. A well-designed mediator will incentivize
agents to report truthfully and follow the recommendation.
A promising and recent tool for mediator design is differential
privacy [18]. The original goal of differential privacy was to protect
individuals privacy in data mining, by ensuring that answering the
same query on two databases differing in a single person’s data leads
to results that are close in some sense. Seen another way, differential
privacy limits any individual’s influence on the result. This can be
1 Contrast

this with dominant strategies: in a truthful auction, no agent can
gain by deviating no matter what the other players play.

quite useful as a tool for mechanism design: If the mediator satisfies
differential privacy, agents will have little incentive to deviate from
truthful behavior since they can only change the selected equilibria
to a small degree.
While this is a theoretically clean idea, there can be practical
issues: currently proposed mechanisms are complex enough that
agents may not be able to verify the promised incentive properties
of the mediator. In general, if agents do not believe the incentive
properties of a mechanism, then they may behave in unpredictable
ways or decline to participate. Indeed, designers of an upcoming
public radio spectrum auction have stressed “obviousness” as a key
feature—the incentive features should be plainly apparent to any
agent [39]. While this is a desirable goal for simple mechanisms,
it is hard to achieve for complex mechanisms. For these cases, we
propose an alternative approach: rather than simplify the mechanism,
use formal verification to automatically check incentive properties.
However, mechanism design poses serious challenges for verification. First, both differential privacy and equilibria properties
are relational properties of programs, which reason about more
than one run of the same program; for instance, truthfulness states
that the payoff of an agent in a run when she reports truthfully is
at least its payoff in a run where she reports arbitrarily. Second,
equilibria properties are significantly more involved than typical
program verification properties. For randomized mechanisms, properties are stated in terms of expected value rather than more standard
equivalences or relations between distributions. Finally, incentive
properties of mediator mechanisms rest on non-trivial interactions
between game-theoretic properties and differential privacy, so their
formal verification must be conducted in a framework that is expressive enough to reason about differential privacy, game-theoretic
properties, and interactions of the two.
Contributions To handle these challenges, we present HOARe2 ,
a type-based framework for relational properties of higher-order
probabilistic programs, like differential privacy, truthfulness, and
approximate equilibrium. HOARe2 is based on refinement types—
an expressive type discipline that captures fine-grained properties of
computations by enriching types with assertions [23]—and tightly
integrates several features: relational refinements [4], refinements at
higher types (where assertions constrain the behavior of functions),
and a polymonadic representation of approximate refinements for
probabilistic computations [3]. We demonstrate the theoretical and
practical relevance of HOARe2 through the following contributions:
2

• We demonstrate that HOARe achieves desirable meta-theore-

tical properties, like soundness with respect to a denotational
semantics (§ 3.3) and semantic subtyping. As a contribution of
independent interest, we show that the logical interpretation of
non-termination adopted by existing refinement type systems is
inconsistent with semantic subtyping when refinements at higher
order types are allowed.
• We define a type-preserving embedding of DFuzz [24]—a

linear dependent type system for differential privacy—into
HOARe2 , and recover soundness of DFuzz from soundness
of HOARe2 (§ 4). The embedding illustrates how semantic
subtyping and refinements at higher types combine to internalize
logical relations in HOARe2 .
• We implement a type-checker for HOARe2 and verify exam-

ples drawn from differential privacy and mechanism design. For
instance, we verify truthfulness properties of randomized auctions, and an equilibrium selection algorithm for aggregative
games based on differential privacy. The implementation is fully
automated, discharging assertions using SMT solvers.
We discuss related work in § 7, and conclude with possible future
directions in § 8.

2.

Relational refinements, informally

We will establish properties of programs by using refinement types,
an expressive typing discipline introduced by Freeman and Pfenning
[23]. As is typical in refinement type systems, we type expressions
in two steps. First, we define a simply typed system in which the
type of probabilistic computations are modeled using a probability
monad Mr¨s; for example, the expected value of a positive realvalued function w.r.t. a distribution is modeled by a function E of
`
type: MrT s Ñ pT Ñ R` q Ñ R , where R` denotes the type of
`
positive reals and R denotes R` extended with `8.
Next, we define a relational refinement type system for simply
typed expressions. Relational refinements [4] specify properties
of pairs of values via types of the form tx :: T | φu, where φ
is a relational assertion: a logical formula that can express facts
involving the left instance xŸ and the right instance xŹ of x. For
instance, the type tx :: N | |xŸ ´ xŹ | ď ku models pairs of natural
numbers which differ by at most k.
Both traditional and relational refinement type systems (e.g., [4])
often forbid refinements at higher types, like tx :: T | φu where T is
a function type. However, such relational refinements are convenient
to model properties of probabilistic operators. For instance, given
a distribution µ :: MrT s, the following types for E µ capture
monotonicity and linearity of expectation:
`

tf :: T Ñ R` | @z.fŸ z ď fŹ zu Ñ tr :: R | rŸ ď rŹ u
`

tf :: T Ñ R` | @z.fŸ z “ k¨fŹ zu Ñ tx :: R | xŸ “ k¨xŹ u
Relational refinements can also be used to model relations between
pairs of distributions, like differential privacy. A probabilistic computation F : T Ñ U is p, δq-differentially private (w.r.t an adjacency
relation Φ) if for every t1 , t2 P T , and for every subset of outputs
E,
t1 Φ t2 ùñ

Pr rx P Es ď exppq

xÐF t1

Pr rx P Es ` δ.

xÐF t2

The parameters  and δ are non-negative real numbers controlling
the strength of the privacy guarantee. Using relational refinement
types, the type of p, δq-differentially private computations from T
to U is:
tx :: T | xŸ Φ xŹ u Ñ tµ :: MrU s | ∆ pµŸ , µŹ q ď δu,
where
ˆ
∆ pµ1 , µ2 q “ max
EĎU

˙
Pr rx P Es ´ exppq Pr rx P Es

xÐµ1

xÐµ2

is the -distance [3] between two distributions µ1 and µ2 over U .
However, this modeling is not appropriate for practical program
verification; indeed, the definition of -distance uses probabilities
and exponentials; it is possible to formalize basic properties for
these concepts, but more advanced reasoning, which is required for
some examples, is beyond the abilities of SMT solvers. Instead, we
introduce a probabilistic polymonad [33], with a type constructor of
the form M,δ r¨s and two operators unit and bind with respective
types:
unit
bind

:
:

T Ñ M,δ rT s
M,δ rT s Ñ pT Ñ M1 ,δ1 rU sq Ñ M`1 ,δ`δ1 rU s.

The main advantage of the polymonad versus the explicit formalization of -distance is that all reasoning about probabilities is confined
to the definition of valid judgment, and to the proof of soundness of
the monadic rules. On the other hand, the refinement types T and U
remain standard relational refinements, and do not need to refer to
probabilities or exponentials.
The interpretation of M,δ r¨s is based on a lifting operator
L,δ p¨q that turns a relation Ψ on T1 ˆT2 into a relation L,δ pΨq on
MrT1 sˆMrT2 s; we will provide the formal definition in § 3.4.

A useful property of lifting [3] is that two distributions are related
by L,δ p“q iff their -distance is upper bounded by δ. In particular,
p, δq-differentially private computations can be modeled by the
relational refinement:
tx :: T | xŸ Φ xŹ u Ñ M,δ rty :: U | yŸ “ yŹ us,
which leads to simpler verification conditions over individual outputs rather than sets of outputs.
Another advantage of this polymonadic approach is that the type
of the bind operator captures the sequential composition theorem of
differential privacy [18], and that it leads to an elegant type system
in which quantitative reasoning related to differential privacy is
confined to the rules of the polymonad. This is in contrast to some
prior work where quantitative reasoning is pervasive in all rules of
the system [3].
The last component of HOARe2 is a monad Cr¨s to model
diverging computations. While this is quite standard, this approach
is key to reconcile semantic subtyping, and refinements at higher
types. We elaborate on this point next.
2.1

An aside on non-termination and refinement types

Exploiting the power of refinement types requires the ability to draw
useful inferences from assertions. These inferences are typically
represented in typing derivations via a subtyping relation ĺ, and
applied with a special typing rule, called subsumption, that changes
the type of an expression to an arbitrary supertype. Ideally, the subtyping relation should be complete w.r.t. the denotational semantics
of the type system—a property known as semantic subtyping. However, extending most existing refinement type systems with semantic
subtyping can lead to an inconsistency, because semantic subtyping
conflicts with typical logical treatments of non-termination.
Inconsistency can arise both in non-relational and relational
settings; let us consider the non-relational case. Here, inconsistency
manifests itself as an expression of type tx : N | Ku in the empty
context, with the expression reducing to a value. Existing refinement
type systems such as F7, F‹ and L IQUID H ASKELL assign the
type tx : N | x ‰ 0u Ñ ty : N | Ku to any recursive function
f that does not terminate on values x ‰ 0, such as for instance
letrec g x “ case x with r0 ñ 0 | s y ñ g xs. On the other
hand, semantic subtyping validates the equivalence F UN -S UB:

solve the issue by internalizing size types into refinement types to
enforce termination.

3.

The HOARe2 System

3.1

Expressions

HOARe2 is a relational type discipline for a λ-calculus with inductive types, unbounded recursion and monads for probabilities and
partiality. For readability, we only present our calculus with some
fixed inductive types.
Let X “ tx, y, . . .u be a countably infinite set of variables.
The set PCFpX q of expressions with variables in X is defined as
follows:
e ::“
|
|
|

`

x | n P N | α P R | pq |  | ¨ :: ¨ | false | true
e e | λx. e | let x “ e in e | letrecm f x “ e
if e then e else e | case e with r ñ e | x :: x ñ es
eÒ | letÒ x “ e in e | unitM e | bindM x “ e in e,
`

where m P tÓ, ¨u and R stands for R` augmented with the infinity
8. We write PCF for PCFpX q when X is clear from the context.
Most of the syntax is standard. The expressions unitM e and
bindM x “ e in e corresponds to the unit and the multiplication
of the probabilistic monad. Similarly, eÒ and letÒ x “ e in e
corresponds to the unit and the multiplication of the partiality monad.
Finally, we have two expressions for building recursive definitions:
one for terminating programs, the other for non terminating ones.
We distinguish between them by means of the superscript m P tÓ, ¨u.
HOARe2 distinguishes between expressions and relational expressions. The former are used in the subject of typing judgments,
and correspond to the actual programs to which we can assign semantics. The latter are used in assertions.

tx : T | φu Ñ ty : U | ψu » tf : T Ñ U | @x : T.φ ùñ ψrf x{ysu

Definition 3.1 (Expressions and Relational Expressions). Let XR
and XP be two disjoint countably infinite sets of relational and
plain variables. Associated with every relational variable x P XR ,
we have aŤleft instance xŸ and a right instance xŹ . We write
XR ’ for xPXR txŸ , xŹ u and X ’ for XR ’ Y XP . The set of
HOARe2 expressions E is the set of expressions in PCFpXP q. The
set of HOARe2 relational expressions E ’ is the set of expressions
in PCFpX ’ q, where only non-relational variables can be bound.

where we write T » U iff T ĺ U and U ĺ T . It follows that f 0
has the problematic type:

3.2 HOARe2 Types

$ f : tx : N | x ‰ 0u Ñ ty : N | Ku
$ f : tg : N Ñ N | @x : N.x ‰ 0 ùñ Ku
$ f : tg : N Ñ N | @x : N.Ku
$ f : N Ñ tx : N | Ku
$ f 0 : tx : N | Ku,

We introduce the types of HOARe2 in two steps. First, we introduce
simple types; for simplicity, we restrict instances of inductive types
to base types. Then, we introduce relational refinement types, which
express properties about two interpretations of an expression.
$0:N

where the first three inferences are by subsumption (the first two
by F UN -S UB, and the second by the standard rule of consequence—
replacing an assertion by a logically weaker one).
This example shows that a naive combination of semantic subtyping with refinements at higher types is inconsistent with the use of
K to model diverging computation. We will follow a more semantically correct approach, by modeling non-termination as a (monadic)
effect using a monad Cr¨s that distinguishes non-terminating and
terminating computations. In this way, the inconsistency is avoided.
We conclude this discussion by noting that this counterexample
is independent of the evaluation strategy. Accordingly, it complements the recent observation by Vazou et al. [52] that a logical
interpretation of non-termination is unsound for call-by-name, even
in languages without higher-order refinements. Vazou et al. [52]

Definition 3.2 (Types). The sets Ty and CoreTy of (simple)
types and core (simple) types are defined as follows:
τ, σ, . . . P Ty

::“

τr | Mrτ s | Crτ s | τ Ñ σ

τr, σ
r , . . . P CoreTy

::“

‚ | B | N | R | R | τr list.

`

The type Mrτ s corresponds to the probability monad over the
type τ , while the type Crτ s corresponds to the partiality monad over
the type τ . Besides the standard function types τ Ñ σ, the type
language includes the unit type, booleans, integers, reals and lists.
Relational types extend the grammar of simple types with
relational refinements, and use a dependent function type rather
than standard function types.
Definition 3.3. The sets of relational types T “ tT, U, . . .u and
assertions A “ tφ, ψ, . . .u are defined as follows:

JΓ $ eÒ : Crτ sKθ = JΓ $ e : τ Kθ

T, U P T ::“ τr | M,δ rT s | CrT s | Πpx :: T q. T | tx :: T | φu
φ, ψ P A ::“ Q px : τ q. φ
px P XP q
Q px :: T q. φ
px P XR q
Cpφ1 , . . . , φn q | e’ “ e’ | e’ ď e’
C “ tJ{0, K{0, {1, _{2, ^{2, ñ{2u,

JΓ $ letÒ x “ e1 in e2 : CrσsKθ =
"
K
if d “ K
JΓ $ e2 : CrσsKθxd otherwise
where d “ JΓ $ e1 : Crτ sKθ
"
1 if x “ JeKθ
JΓ $ unitM e : Mrτ sKθ = x ÞÑ
0 otherwise

where , δ, e’ P E ’ , and Q P t@, Du.
The definitions of relational types and assertions are mutually
recursive. For the latter, the constructors Cr.s and M,δ r.s capture
the partiality monad and the probability polymonad for relational
refinements. The type Πpx :: T q. U corresponds to the dependent
type product of T over U indexed by x. As usual, we write T Ñ U
for Πpx :: T q. U when x does not occur free in U . A type of the
shape tx :: T | φu refines the type T using the assertion φ. In both
dependent and refinement types, we require the bound variable to
be relational (x P XR ).
Assertions are built from primitive assertions using the standard
connectives and quantification; we allow quantification over both
relational and plain variables. Primitive assertions are equalities and
inequalities over relational expressions.
The notions of substitutions are defined largely as usual. Substitutions bind pairs of (non-relational) expressions to relational
variables, and involve a special treatment of refinement type constructors, which must handle the relational expressions. For instance,
for a substitution ρ “ ty ÞÑ pe1 , e2 qu, we define
ˇ "
"
**
ˇ
y ÞÑ |e1 |Ÿ
tx :: T | φuρ “ x :: T ρ ˇˇ φ Ÿ
,
yŹ ÞÑ |e2 |Ź
where |e|Ÿ (resp. |e|Ź ) is obtained from e by replacing all the free
variables x of e by xŸ (resp. xŹ ).
3.3

Standard typing

We define the simply typed layer of HOARe2 , and prove its soundness w.r.t. a denotational semantics. Both the type system and the
semantics are mostly standard.
Static semantics The sole notable typing rules are for the two
different letrec of our language:
L ET R EC

L ET R EC SN

Γ, f : τ Ñ Crσs $ λx. e : τ Ñ Crσs
Γ $ letrec f x “ e : τ Ñ Crσs

Γ, f : τ Ñ σ $ λx. e : τ Ñ σ

SN -guard

Γ $ letrecÓ f x “ e : τ Ñ σ.
The rule L ET R EC handles unrestricted recursion, and requires that
the output type be in the partiality monad. On the contrary, the rule
L ET R EC SN does not impose any restriction on the type, but the
expression must pass a termination guard. We leave the termination
guard unspecified; possible forms of enforcing the guard include
sized types and syntactic criteria.
Denotational semantics The denotational semantics is largely
standard. Core types are interpreted in the standard way. The
interpretation of types mixes a set-theoretical and cpo semantics in
order to accommodate the partiality monad.
Definition 3.4 (Interpretation of types). The interpretation Jτ K of a
type τ P Ty is inductively defined as follows:
ř
JMrτ sK “ tµ : Jτ K Ñ R` | dsupppµq discrete ^ xPτ µ x “ 1u
JCrτ sK “ Jτ KK

Jτ Ñ σK “ Jτ K ( JσK,

where the support dsupppµq of a distribution µ is the set of elements
for which µ takes a non-zero value, and ( represents a cpo-

JΓ $ bindM x “ e1 in e2 : MrσsKθ =
ř
d ÞÑ gPJτ K pJe1 Kθ pgq ˆ Je2 Kθxg pdqq
Ť
JΓ $ letrecm f x “ e : τ Ñ σKθ = nPN F n pKJτ ÑσK q

where F pdq “ JΓ, f : τ Ñ σ $ λx. e : τ Ñ σKθd
f

Figure 1: Interpretation of PCF Expressions

continuous function space when the codomain is equipped with
a cpo structure, and the set-theoretical function space otherwise.
Types Crτ s and σ Ñ τ where τ is interpreted as a cpo are
interpreted as cpos. However, types of the form Mrτ s are not
interpreted as cpos, because their interpretation is based on discrete
distributions.2
We can now define the denotational interpretation of expressions.
Ť
Definition 3.5. A valuation θ is any finite map from X to τ Jτ K.
A valuation θ validates an environment Γ, written θ ( Γ, if @x P
dompΓq, xθ P JxΓK. We denote by JΓ $ e : τ Kθ the interpretation
of Γ $ e : τ with respect to θ ( Γ.
The definition of the interpretation is mostly standard; Figure 1
gives the interpretation of the monadic constructions and of the two
letrec operators. As expected, the static semantics is sound w.r.t
the denotational one.
Lemma 3.1. If Γ $ e : τ and θ ( Γ, then JeKθ P Jτ K.
3.4

Refinement Typing

The key point of relational typing is its ability to relate a pair
of expressions—which we call the left and right expressions—via
relational assertions that appear as refinements in types. For instance,
the type
Πpx :: Nq. ty :: N | yŸ “ xŸ ` 1 ^ yŹ “ xŹ u
represents a pair of integer to integer functions where the left
function adds 1 to argument, and the right one returns its argument
untouched.
In this section, we define the refinement type system of HOARe2
in three steps. First, we give an interpretation for assertions and
refinement types. Second, we define a subtyping relation that is
complete w.r.t. this interpretation. Finally, we define the refinement
type system, and prove its soundness w.r.t. a denotational semantics.
We start by defining relational contexts.
Definition 3.6. A relational environment G is any finite sequence
of relational bindings px :: T q s.t. a variable is never bound twice
and only variables of XR are bound. We use H to denote the empty
environment. A relational environment defines a finite mapping from
2 It

would have been possible to interpret them as sub-distributions and to
define another letrec operator for probabilistic computations, at the cost
of replacing δ ` δ 1 by expp1 q δ ` exppq δ 1 in the typing rule for bind.
However, our examples do not require this additional generality.

JCpφ1 , . . . , φn qKθ “ CpJφ1 Kθ , . . . , Jφn Kθ q
’
’
’
Je’
1 “ e2 Kθ “ Je1 Kθ “ Je2 Kθ

Je’
1

ď

e’
2 Kθ

“

Je’
1 Kθ

J@ px : τ q. φKθ “

Ź

JD px : τ q. φKθ “

Ž

J@ px :: T q. φKθ “

JD px :: T q. φKθ “

ď

Je’
2 Kθ

!
)
pd1 ,d2 qPLT Mθ JφKθ xŸ ÞÑ d1
xŹ ÞÑ d2

Figure 2: Relational interpretation of assertions

xŹ ÞÑ d2

pd1 , d2 q P Ltx :: T | φuMθ

xŹ ÞÑ d2

pf1 , f2 q P LΠpx :: T q. U Mθ

d
dPJτ K JφKθx
Ž

where C stands for the C-boolean operator.

JφKθ!xŸ ÞÑ d1 )

pf1 , f2 q P J|T | Ñ |U |K2
@pd1 , d2 q P LT Mθ . pf1 pd1 q, f2 pd2 qq P LU Mθ!xŸ ÞÑ d1 )

d
dPJτ K JφKθx

Ź

!
)
pd1 ,d2 qPLT Mθ JφKθ xŸ ÞÑ d1
xŹ ÞÑ d2

pd1 , d2 q P LT Mθ

τ K2
pd1 , d2 q P Jr
τ Mθ
pd1 , d2 q P Lr

pd1 , d2 q P LT Mθ Y tpK, Kqu
pd1 , d2 q P LCrT sMθ

µ1 , µ2 P Mr|T |s
L,δ pLT Mθ q µ1 µ2
pµ1 , µ2 q P LM,δ rT sMθ

Figure 3: Relational interpretation of types
variables to relational types; we write xG for the application of the
finite map G to x.
We define a type erasure function |¨| from relational to simple
types, which maps dependent products to function spaces, and
erases refinements and the indexes of the probabilistic monad.
The definition of |¨| extends recursively to relational environments:
x|G| “ |xG| for any x P dompGq. We also define the relational
type erasure of G, written }G}, by xs }G} “ x|G| iff x P dompGq,
where s P tŸ, Źu. Note that given a relational binding px :: T q,
the relational type erasure }px :: T q} gives the environment pxŸ :
|T |, xŹ : |T |q.
Next, we interpret assertions and refinement types.
Definition 3.7 (Relational interpretation of refinement types). We
say that a valuation θ validates a relational environment G, written
θ ( G, if θ ( }G} and @x P dompGq, pxŸ θ, xŹ θq P LxGMθ .
Figures 2 and 3 define the relational interpretation JφKθ P tJ, Ku
(resp. LT Mθ P J|T |K2 ) of an assertion φ (resp. of a relational type T )
w.r.t a valuation θ ( Γ (resp. θ ( }G}).
Assertions are interpreted relationally in the expected way
where some care is needed for quantifiers since the interpretation
distinguishes between binders for relational and plain variables.
Relational types are interpreted as sets of pairs of elements of the
interpretation of the erased type. Formally, a pair pd1 , d2 q is in the
relational interpretation of a refinement tx :: T | φu if the assertion
φ holds in a relational context where d1 and d2 are assigned to xŸ
and xŹ , respectively.
The relational interpretation of the dependent product is defined
in a logical relation style: it relates function elements f1 , f2 that
map related elements d1 , d2 (in LT Mθ ) to related elements (in
LU Mθ!xŸ ÞÑ d1 ) ). A monadic type CrT s is relationally interpreted
xŹ ÞÑ d2

as the set of pairs in the interpretation of T plus the pair pK, Kq. The
polymonadic type M,δ rT s is interpreted using a lifting construction
L,δ p¨q that turns a relation Ψ on T1 ˆT2 into a relation L,δ pΨq on
MrT1 sˆMrT2 s.

Definition 3.8 (Lifting of a relation). Given Ψ Ď T1 ˆT2 , we have
L,δ pΨq µ1 µ2 iff there is a distribution µ P MrT1 ˆ T2 s such that
1. µ pa, bq ą 0 implies pa, bq P Ψ,
2. π1 µ ď µ1 ^ π2 µ ď µ2 , and
3. ∆ pµ1 , π1 µq ď δ, ^∆ pµ2 , π2 µq ď δ ,
ř
ř
where π1 µ “ λx. y µ px, yq and π2 µ “ λy. x µ px, yq.
We next define subtyping between refinement types.
Definition 3.9 (Subtyping). The subtyping relation G $ T ĺ U is
defined by the rules of Figure 4.

S UB -R EFL

G$T
G$T ĺT
S UB -L IST

S UB -C

G$T ĺU
G $ T list ĺ U list

G$T ĺU
G $ CrT s ĺ CrU s

S UB -R IGHT

S UB -T RANS

G$T ĺU
G$U ĺV
G$T ĺV

S UB -L EFT

G $ tx :: T | φu
G $ tx :: T | φu ĺ T

G$T ĺU
}G, x :: U } $ φ
@θ. θ ( G, x :: T ñ JφKθ
G $ T ĺ tx :: U | φu
`

`

G$T ĺU
}G} $ i : R
}G} $ δi : R
@θ. θ ( G, x :: T ñ J1 ď 2 ă 8 ^ δ1 ď δ2 ă 8Kθ
S UB -M
G $ M1 ,δ1 rT s ĺ M2 ,δ2 rU s
S UB -P ROD

G $ T2 ĺ T1
G, x :: T2 $ U1 ĺ U2
G $ Πpx :: T1 q. U1 ĺ Πpx :: T2 q. U2
Figure 4: Relational Subtyping

A subtyping judgment G $ T ĺ U relates only relational
types that erase to the same simple type, i.e. |T | “ |U |. The
rules S UB - LEFT and S UB - RIGHT allow erasing and reinforcing
refinements. The rule S UB -M allows weakening the indices of the
probabilistic polymonad, and the underlying refinements. Other
rules are mostly standard. The definition of subtyping validates the
relational counterpart of the equivalence F UN -S UB discussed in § 2.
More generally, it is possible to define a normalization function that
converts any refinement type T into an equivalent type tx :: U | φu,
where U is a simple type, i.e. does not contain any refinement.
The existence of the normalization function immediately entails
semantic subtyping.
Finally, we present the HOARe2 typing rules.
Definition 3.10 (Relational Typing). The refinement typing relation
G $ e1 „ e2 :: T is defined in Figure 5. We use Γ $ e :: T as a
shorthand for Γ $ e „ e :: T .
We briefly comment on some of the typing rules. As in relational Hoare logic [6], we distinguish between synchronous and
asynchronous rules; the latter operate on both expressions of the

VAR

x P dompGq
G $ x :: xG

L ET R EC SN

C ASE

A BS

G, x :: T $ e :: U
G $ λx. e :: Πpx :: T q. U

A PP

G, f :: Πpx :: T q. U $ λx. e :: Πpx :: T q. U
G $ Πpx :: T q. U
SN -guard
G $ letrecÓ f x “ e :: Πpx :: T q. U

G$T
G $ e1 :: T

L ET R EC

G $ Πpx :: T q. CrU s
G, f :: Πpx :: T q. CrU s $ λx. e :: Πpx :: T q. CrU s
G $ letrec f x “ e :: Πpx :: T q. CrU s

G $ e :: τr list
@θ. θ ( G ñ Jp|e|Ÿ “ q ô p|e|Ź “ qKθ
G, x :: τr, y :: τr list, t|e|Ÿ “ xŸ :: yŸ ^ |e|Ź “ xŹ :: yŹ u $ e2 :: T
G $ case e with r ñ e1 | x :: y ñ e2 s :: T

G $ e1 :: CrT1 s
G $ CrT2 s
G, x :: T1 $ e2 :: CrT2 s
B IND C
G $ letÒ x “ e1 in e2 :: CrT2 s

`

U NIT M

G $ e1 :: M1 ,δ1 rT1 s
G, x :: T1 $ e2 :: M2 ,δ2 rT2 s
G $ M2 ,δ2 rT2 s
B IND M
G $ bindM x “ e1 in e2 :: M1 `2 ,δ1 `δ2 rT2 s
AR ED L EFT

AC ASE

G $ e1 :: Πpx :: T q. U
G $ e2 :: T
G $ e1 e2 :: U tx ÞÑ e2 u

U NIT C

G $ e :: T
G $ eÒ :: CrT s

`

}G} $  : R
}G} $ δ : R
G $ e :: T
G $ unitM e :: M,δ rT s

S UB

G $ e :: T
G$T ĺU
G $ e :: U

e1 Ñ e11
G $ e1 „ e2 :: T
G $ e11 „ e2 :: T

G$T
|G| $ e : τr list
|G| $ e1 : |T |
G, t|e|Ÿ “ u $ e1 „ e1 :: T
G, x :: τr, y :: τr list, t|e|Ÿ “ xŸ :: yŸ u $ e2 „ e1 :: T
G $ case e with r ñ e1 | x :: y ñ e2 s „ e1 :: T
Figure 5: Relational Typing (Selected Rules)

Example

judgments, whereas the former operate on a single expression and
can relate expressions that have different shapes. Synchronous rules
exist for the two monads, the two letrec and the dependent product. Note that the rule for application substitutes the argument of
the application into the result type, and does not impose any value
restriction.
The case construction is an example of a rule with both a
synchronous and an asynchronous version. The synchronous rule
requires a synchronicity condition: the same branch must be taken
in the left and right expressions. For the case of lists, this is ensured
by requiring that the matched lists are either both empty or both
non-empty. In contrast, the asynchronous rule does not require this
condition. The reduction rules close typing under reduction, and is
useful to relate expressions that do not have the same shape.
Refinement typing is sound w.r.t. its denotational semantics.
Theorem 3.1 (Soundness). If G $ e1 „ e2 :: T , then for every
valuation θ |ù G we have pJe1 Kθ , Je2 Kθ q P LT Mθ .
It follows that HOARe2 accurately models differential privacy.

Corollary 3.1 (Differential Privacy). If $ e :: tx :: σ | Φu Ñ
M,δ rty :: τ | yŸ “ yŹ us then JeK is p, δq-differentially private
w.r.t. adjacency relation JΦK.

We have completed a formalization of Theorem 3.1 in the Coq
proof assistant, assuming an axiomatization of probabilities and
lifting.
3.5

histogram
dummysum
noisysum
two-level-a
two-level-b
binary
idc
dualquery
competitive-b
competitive
fixedprice
summarization

# Lines
25
31
55
38
56
95
73
128
81
75
10
471

Verif. time
2.66 s.
11.95 s.
3.64 s.
2.55 s.
3.94 s.
18.56 s.
27.60 s.
27.71 s.
2.80 s.
4.19 s.
0.90 s.
238.42 s.

Table 1: Benchmarks
inductive datatypes, let expressions, as well as the ability to define
logical predicates and core theories for the datatypes.
All the programs presented in § 5 and § 6, as well as some additional examples from the DP literature (private histograms, sums,
two level counters and IDC) were automatically type checked by
the implementation, with the only help of top-level type annotations.
See Table 1 for a summary.
Both the type-checker and the Coq formalization are available at
https://github.com/ejgallego/HOARe2/.

Type-checking

We have implemented a type-checker for HOARe2 . The typechecker generates proof obligations during type-checking; proof
obligations are sent to SMT solvers via Why3. The type-checker
uses a ML-like syntax and includes a few practical extensions like

4.

Embedding DFuzz

DFuzz [24] is a linear dependently typed language that has been
used to verify many examples of differential private algorithms. In
this section, we define a type-preserving embedding from DFuzz

κ
S
R
σ, τ
e
Γ, ∆
φ, ψ
Φ, Ψ

::“
::“
::“
::“
|
::“
|
|
::“
::“
::“

r|n
(kinds)
i|0|S`1
(sizes)
i | S | Rě0 | 8 | R ` R | R ¨ R(sensitivities)
R | RrRs | σ listrSs |!R σ ( τ
(types)
@i : κ. σ | MrRs
x | N | Rě0 | λx. e
(expressions)
letrec f x “ e | e1 e2 | Λi. e | erRs
case e with r ñ e1 | x :: xsris ñ e2 s
H | Γ, x :!R σ
(environments)
H | φ, i : κ
(sens. environments)
H | S “ 0 | S “ i ` 1 | Φ, Φ (constraints)

Figure 6: DFuzz Types and Expressions

into HOARe2 , and recover soundness of DFuzz from Theorem 3.1.
The embedding is interesting for several reasons. First, it shows that
HOARe2 is sufficiently expressive to capture all differentially private examples covered by DFuzz. Second, it relates two previously
disconnected approaches for verifying differential privacy. Third, it
shows how relational refinements can internalize logical relations.
For compactness, we only consider a terminating fragment
of DFuzz with probabilities only over real numbers. Types and
expressions are defined in Figure 6; both are parameterized by
indexes, drawn from two distinct languages. The first one deals
`
with sensitivities (interpreted as elements of R ) and the second one
deals with sizes (interpreted as natural numbers). Typing judgments
are of the form φ; Φ; Γ $D e : σ, where φ is an environment that
records the sensitivity and size variables, Φ is a set of constraints
used in pattern matching, and Γ is an environment containing
assignments of the form x :!R τ . Figure 7 gives selected typing
rules, where environments are combined by algebraic operations.
The environment R ¨ Γ is obtained by taking x :!R¨Ri τ for every
x :!Ri τ P Γ, while environment addition is defined as:
px :!R1 σ, Γq ` px :!R2 σ, ∆q “ x :!R1 `R2 σ, pΓ ` ∆q
px :!R σ, Γq ` ∆ “ x :!R σ, pΓ ` ∆q
if x R domp∆q
Γ ` px :!R σ, ∆q “ x :!R σ, pΓ ` ∆q
if x R dompΓq.
We refer to Gaboardi et al. [24] for definitions and further explanation of the typing rules.
In DFuzz, types σ, τ are interpreted as metric spaces, with
associated metrics dσ , dτ . Then, the DFuzz type system enforces
metric preservation [24, 48]: if e is well typed in context Γ, for
arbitrary closing substitutions θ1 , θ2 for Γ, the distance between the
interpretations of θ1 peq and θ2 peq is upper bounded by the distance
between θ1 and θ2 . As a particular instance, DFuzz expressions of
type !R σ ( τ correspond to R-sensitive functions, i.e. functions
f such that for every pairs of inputs v1 and v2 , dτ pf v1 , f v2 q ď
R ¨ dσ pv1 , v2 q. We will present an embedding which captures metric
preservation as a relational refinement type.
To this end, we first define the multiplication operation on
sensitivities in more detail. We distinguish two sorts: sensitivities
Rs “ Rą0 Y t0s , 8u and distances Rd “ Rą0 Y t0d , Ku. We
interpret sensitivities R in DFuzz as sensitivities, while metrics
(Figure 8) are interpreted as distances. We write s and d to range
over the respective sorts. To interpret multiplication, we define a
associative and commutative operator ˛ that maps Rs ˆ Rs Ñ Rs
and Rd ˆ Rs Ñ Rd . The non-standard cases are those involving
0s , 0d and 8, K:
#
0d
if d “ 0d
s˛8“8
d˛8“
K
otherwise
K˛s“K

r ˛ r1 “ r ¨ r1

if r, r1 P R` .

φ; Φ; Γ, x :!1 σ $D x : σ

φ; Φ; Γ, x :!R σ $D e : τ
φ; Φ; Γ $D λx. e :!R σ ( τ

φ; Φ; Γ $D e1 :!R σ ( τ
φ; Φ; Γ1 $D e2 : σ
φ; Φ; Γ ` R ¨ Γ1 $D e1 e2 : τ
φ; Φ; Γ $D e : R
φ; Φ; 8 ¨ Γ $D return e : MrRs
φ; Φ; Γ, f :!8 p!R σ ( τ q, x :!R σ $D e1 : τ
φ; Φ; 8 ¨ Γ $D letrec f x “ e :!R2 σ ( τ
φ, i : κ; Φ; Γ, f :!8 p@i : κ. σq $D e1 : σ
i fresh in Φ, Γ
φ; Φ; 8 ¨ Γ $D letrec f i “ e : @i : κ. σ
φ; Φ; Γ $D e1 : Mrσs
φ; Φ; Γ1 , x :!8 σ $D e2 : Mrτ s
1
φ; Φ; Γ ` Γ $D let x “ e1 in e2 : Mrτ s
φ, i : κ; Φ; Γ $D e : σ
i fresh in Φ, Γ
φ; Φ; Γ $D Λi : κ. e : @i : κ. σ

φ; Φ; Γ $D e : @i : κ. σ
φ |ù S : κ
φ; Φ; Γ $D erSs : σrS{is

φ; Φ; ∆ $D e : σ listrSs
φ; Φ, S “ 0; Γ $D el : σ
φ, i : n; Φ, S “ i ` 1; Γ, x :!R σ, xs :!R σ listris $D er : σ
φ; Φ; Γ ` R ¨ ∆ $D case e with r ñ el | x :: xsris ñ er s : σ
Figure 7: DFuzz typing rules

DR pd1 , d2 q “ |d1 ´ d2 |
$ÿ
&
Dσ pdi1 , di2 q if szpd1 q “ szpd2 q “ S
Dσ listrSs pd1 , d2 q “ iďn
%
K
otherwise
#
0 if d1 “ d2 “ R
DRrRs pd1 , d2 q “
K otherwise
ˆ
˙
Dτ d1 d3 , d2 d4 q
D!R σ(τ pd1 , d2 q “ max
´R ˛ Dσ pd3 , d4 q
d3 ,d4 P|σ|
ˇ ˆ
˙ˇ
ˇ
µ
1 pxq ˇˇ
DMrRs pµ1 , µ2 q “ max ˇˇln
xPR
µ2 pxq ˇ
D@i:κ. σ pd1 , d2 q “ max Dσrd{is pd1 d, d2 dq
dPκ

Figure 8: Metric induced by DFuzz types

Note that ˛ with type Rd ˆ Rd Ñ Rd is never used.
Then, the expression Dσ : |σ| ˆ |σ| Ñ Rd will capture the
distance function for the DFuzz type σ on our embedding, where
| ¨ | is the erasure function from DFuzz types to simple types. For
the sake of readability, we define Dσ in usual mathematical style
(see Figure 8), where sz denotes the length of a list.
The translation ¨˚ is first defined on sensitivities and sizes, then
on types and expressions, and finally on environments. Sensitivities
and sizes are translated directly as expressions of type Rs and N
respectively. More interestingly, the translation for types (given
in Figure 9) uses refinements and dependent products to capture

pRrRsq˚
pσ listrSsq˚
p!R σ ( τ q˚
p@i : κ. σq˚
MrRs˚

“ tx :: R | xŸ “ xŹ “ R˚ u
“ tx :: |σ| list | szpxŸ q “ szpxŹ q “ S ˚ u
“ σ˚ Ñ τ ˚
“ Πpi :: tx :: κ˚ | xŸ “ xŹ uq. σ ˚
“ M0,0 rRs

Corollary 4.1. If H; H; x :! τ $D e : MrRs then
tx :: τ ˚ | DpxŸ , xŹ q ď 1u $ e˚ :: M,0 rty :: R | yŸ “ yŹ us.
Proof. By Theorem 4.1,
x :: τ ˚ $ e˚ :: ty :: M0,0 rRs | DMrRs pyŸ , yŹ q ď DΓ pxŸ , xŹ qu
with Γ ” x :! τ . Let U “ tx :: τ ˚ | Dτ pxŸ , xŹ q ď 1u. By
definition of D and elementary reasoning about probabilities,

Figure 9: Translation of DFuzz types

x :: U $ e˚ :: ty :: M0,0 rRs | ∆ pyŸ , yŹ q ď 0u.
size and sensitivity information. The translation of expressions is
straightforward; the only interesting case are:
˚

˚

perSsq “ e S

˚

˚

pΛi.eq “ λi : κ.e

˚
“ case e˚ with r Ñ e˚
1 | x :: xs Ñ e2 tszpxsq{ius.

The translation of environments is defined inductively. We have
pHq˚ “ H for terms, index environments, and constraints. Moreover, we define:
pΓ, x :!R σq
pφ, i : κq˚
pΦ, S1 “ S2 q

“
“
“

˚

x :: U $ e˚ :: M,0 rty :: R | yŸ “ yŹ us.

˚

pcase e with r Ñ e1 | x :: xsris Ñ e2 sq˚

˚

Finally, by semantic subtyping:

Moreover, Theorem 4.1 and Theorem 3.1 give a direct proof of
metric preservation for DFuzz.
Theorem 4.2 (DFuzz Metric Preservation [24]). If φ; Φ; Γ $D e :
τ and θ |ù φ, Φ and θ1 , θ2 |ù JΓKθ , then
DJτ Kθ pJe˚ Kθ1 ,θ , Je˚ Kθ2 ,θ q ď DJΓKθ pθ1 , θ2 q.

˚

Γ , x :: σ
φ˚ , i :: tx :: κ˚ | xŸ “ xŹ u
Φ˚ , t_ :: B | S1˚ “ S2˚ u.

Note that the translation of size and sensitivity environments requires
the equivalence of the left and right instances of the relational
variables. We can show soundness of the embedding.
Theorem 4.1 (DFuzz Embedding). If φ; Φ; Γ $D e : τ then
˚
φ˚ , Φ˚ , Γ˚ $ e˚ :: ty :: τ ˚ | Dτ pyŸ , yŹ q ď DΓ pΓ˚
Ÿ , ΓŹ qu,
ř
˚
where DΓ pΓ˚
Ÿ , ΓŹ q “
x:!R σPΓ R ˛ Dσ pxŸ , xŹ q.

Proof. By induction on the derivation of φ; Φ; Γ $D e : τ . The
cases for abstraction and application rely on the properties of
semantics subtyping. In particular, using subtyping we can pass
from
Πpx :: σ ˚ q.ty :: τ ˚ | Dτ pyŸ , yŹ q ď
˚
˚
˚
DΓ,x:!R σ ppΓ˚
Ÿ , xŸ :: σ q, pΓŹ , xŹ :: σ qqu

to
˚
tf :: Πpx :: σ ˚ q. τ ˚ | D!R σ(τ pfŸ , fŹ q ď DΓ pΓ˚
Ÿ , ΓŹ qu

and vice versa. Higher order relational refinements are crucial here
for internalizing the metric of DFuzz at the function type that is
essentially a logical relation argument—this equivalence shows
that two functions are related if they map related inputs to related
outputs.
Similarly, for the probability distribution case, remembering that
we consider only distributions over base types, we use subtyping to
pass from
˚
M0,0 rty :: R | DR py1 , y2 q ď DΓ pΓ˚
Ÿ , ΓŹ qus

to
´
¯
˚
tz :: MrRs | L0,0 DR py1 , y2 q ď DΓ pΓ˚
Ÿ , ΓŹ q zŸ zŹ u
and vice versa.
The other cases are similar. Interestingly, the case of pattern
matching does not require asynchronous reasoning. Indeed, the
refinement type of the translation of the term under match ensures
that the two runs will take the same branch.
Hence typable DFuzz expressions are differentially private.

Notice that the above theorem uses three valuations. The valuation θ is used for index variables which are equal in the two
executions. The other two valuations θ1 , θ2 are used to substitute
related values in the two executions.

5.

Differential Privacy

Theorem 4.1 establishes that every differentially private algorithm
that can be modeled in DFuzz is also captured by HOARe2 . In
addition, we present a few previously unverified algorithms demonstrating the features of our system.
In what follows, we will use some notational shorthands. We
write mlet/munit, clet/cunit for the bind/return operations of the
probabilistic and partiality monad. We write Rě for the type
tx :: R | xŸ ě xŹ u. When a relational variable x is assumed
to be equal in both runs (xŸ “ xŹ ), we omit the projection and
write x for both xŸ and xŹ .
5.1

Private Primitives

We review two differentially private mechanisms that are used in the
next algorithms. The first mechanism is the Laplace mechanism [7],
which releases a private version of a numeric value (which can
differ in the two runs) by adding noise drawn from the Laplace
distribution.
Formally, the -private Laplace mechanism takes a real number
x as input and returns x ` ν, where ν is random noise drawn from
the Laplace distribution, which has density function

F pνq “ exp p´|ν|q .
2
If x can differ by at most s in adjacent runs, then the Laplace
mechanism is ps, 0q differentially private. We model this as an
operator lap with the following type:
Πpx :: Rq. M |xŸ ´xŹ |,0 rtu :: R | uŸ “ uŹ us.
When the output range is non-numeric, a typical tool from
differential privacy is the Exponential mechanism [38]. Let B be
the output range, and suppose there is a quality score Q : B Ñ
A Ñ R. On an input a, the exponential mechanism produces b P B
approximately maximizing Q b a. If for every b P B and adjacent
a1 , a2 P A (wrt. an adjacency relation Φ), the quality score Q
satisfies the condition
|Q b a1 ´ Q b a2 | ď s,

then the Exponential mechanism satisfies ps, 0q-differential privacy.
We model this as an operator expmech of type
ta :: A | aŸ Φ aŹ u Ñ S Ñ Ms,0 rtb :: B | bŸ “ bŹ us
with the type S of score functions defined as
tb :: B | bŸ “ bŹ u Ñ ta :: A | aŸ Φ aŹ u
Ñ tr :: R | |rŸ ´ rŹ | ď su .
5.2

Dual Query Release

We first focus on the problem of privately answering a large set
of queries. The Laplace mechanism is a simple solution, but
? it’s
known that this will add noise to each query proportional to k for
k queries under p, δq-privacy. When k is large, the large noise will
make the released answers completely useless. Fortunately, there is
a line of algorithms where noise is added in a carefully correlated
manner, guaranteeing privacy while adding noise proportional only
to log k. We have verified the privacy of one such algorithm,
called DualQuery [25]. The algorithm is parameterized by a natural
number s and a set qs of queries to answer accurately. The input is
the number of rounds t and database db, and the output is a private
synthetic database that is accurate for the given queries. The code
of the algorithm is given below:
let rec dualquery t db = match t with
| 0
Ñ munit []
| 1 + t’ Ñ
mlet curdb
= dualquery t’ db
let quality
= build_quality t’ curdb
mlet e
= expmech db quality
mlet new_qry
= sampleN s e
let newrecord = opt new_qry
munit (newrecord :: curdb)

tt :: N | tŸ “ tŹ u
tdb :: N list | DN list pdbŸ , dbŹ q ď 1u
Ms¨t2 ¨,0 rtl :: N list | lŸ “ lŹ us.

The type states that for two runs with adjacent databases, dualquery
will return synthetic databases that are s ¨ t2 ¨  apart, where t is the
number of iterations and s is the number of samples used.

Private Counters and the Partiality Monad

Our second example is a private counter. The program takes in a list
of real numbers, and releases a list of running counts. This algorithm
is also known as the binary mechanism due to Chan et al. [11] and
has not been verified before; previous verification work focused on
the two-level counter from the same paper.
Suppose the input stream has length T “ 2n . The binary
mechanism will return a list of noisy sums, reusing noise to reduce
the improve the accuracy of the sums. The algorithm proceeds via
branching recursion. In the base case, we add Laplace noise to the
single element of the input stream and return. In the recursive case,
we split the input stream into a first and a second half and perform
the recursive call on each half; we then return the noised sum of the
whole stream together with the result of the recursive calls. Each
output list contains the sums for one “level” of the tree; the first list
contains a single sum of length 2n , the next contains the two sums
of length 2n´1 , and so on.
The algorithm terminates, but the simple guard condition implemented in our tool does not capture termination.3 Hence its
formalization is based on the partiality monad and its associated
cunit and clet operations:
let rec binary n ls
| []
Ñ cunit
| x :: xs
Ñ match
| []
Ñ cunit

= match l with
(munit [])
xs with
(mlet sum = lap x in
munit ([sum] :: []))

| y :: ys Ñ
let (left, right) = split l in
clet cleftN
= binary (n - 1) left in
clet crightN
= binary (n - 1) right in
cunit(mlet leftN = cleftN
in
mlet rightN = crightN
in
mlet sum
= lap (sum l)
in
munit ([sum] :: (leftN ++ rightN)))

in
in
in
in
in

We encode the database as a list of natural numbers; adjacent
databases are lists of the same length whose distance w.r.t. DN list
is smaller than 1. Here we consider DN list to be defined similarly
to the distance Dσ listrns for list of size n defined in Figure 8 but
where the n is provided implicitly by the length of the lists. We
represent the output of the mechanism as a list of selected records,
each encoded as a natural number.
The algorithm performs t steps, producing one record of the
synthetic database in every round. For each round, we first build a
quality score quality—a function from queries to real numbers—
based on the previously produced records, using the auxiliary function build_quality. If we think of the current records as forming
an approximate database, the quality score measures how poorly the
approximation performs on each query. We then sample s queries
using the exponential mechanism with this quality score; queries
with higher error are more likely to be selected. These queries are
fed into an optimization function opt, which chooses the next record
to add to the approximate database.
The only private operation is the exponential mechanism. The
quality score we generate at each round i has sensitivity i, and so a
draw form the exponential mechanism is i-private. Since i is upper
bounded by t and there are s samples per round, the privacy cost
per round is bounded by s ¨ t ¨ . With t rounds in total, the whole
algorithm is s ¨ t2 ¨ -private. This guarantee is reflected in the type
of dualquery:
Ñ
Ñ

5.3

The algorithm binary takes as input a natural number n and a list
n
ls of reals with length 2 and returns a list of lists of reals. Formally,
binary has type
tn :: N | nŸ “ nŹ u
Ñ tl :: R list | szplŸ q “ szplŹ q “ 2n ^ DR list plŸ , lŹ q ď ku
Ñ CrM¨k¨pn`1q,0 rtl :: pR listq list | lŸ “ lŹ uss,
where we write n for readability (since it is assumed equal in both
runs) and where we use DR list to the distance of lists at the type
R list (defined analogously to DN list ).

6.

Auctions and Algorithmic Game Theory

We now study the verification of mechanisms with incentive properties. We start by describing the truthfulness property for deterministic mechanisms, then we proceed to the randomized case. The
closing examples illustrates the problem of computing an approximate Nash equilibrium using differential privacy.
6.1

Truthful auctions

In the digital goods setting, there is an infinite supply of identical
goods to be sold in auction. For instance, when selling music
downloads, goods can be reproduced for free. We assume every
agent (or bidder) i has a secret value vi , which is the price she
values the item, and submits a single bid bi to the mechanism. Once
all bids have been submitted, the mechanism selects a set of winning
bidders and prices pi for each winner. Bidders aim to maximize
their utility, which is 0 if they do not win and vi ´ pi if they win
and at price pi .
3 It is of course possible to prove termination using known techniques, but
we want to demonstrate the partiality monad.

We want our mechanism to be truthful: given fixed bids of the
other agents b´i , the utility of agent i is maximized when she bids
her true valuation bi “ vi . This feature makes bidding easy for
bidders, and provides the algorithm designer with some assurance
that she will see the correct inputs (the true values of the players).
From a verification point of view, truthfulness is a relational property
of programs: if the mechanism maps bids to outcomes and all but
one of the bidders bids the same in both runs, then the remaining
bidder should have higher utility when bidding truthfully than when
bidding non-truthfully.
We start with the fixed-price auction, a very simple mechanism
for this setting. First, we pick a price p (the reserve price). Bidders
then submit their bids, and we select all bidders who bid above p to
be winners. Each winning bidder is charged price p.
Informally, this process is truthful: a bidder’s price does not
depend on her own bid, so lowering her bid will never lower the
price—it can only cause her to lose the item at a price that she would
have wanted to pay. Similarly, increasing her bid above her value is
never beneficial: If her truthful bid is winning, raising her bid does
not change the outcome (she still wins, and pays the same price). If
her truthful bid is losing, raising her bid can only cause her to win
the item at a price that is higher than her value.
To model this with code, we will model a single bidder’s utility
when she deviates.4 Note that each bidder is treated independently—
her utility depends solely on her value, her bid, and the reserve price,
and not on what any of the other bidders do. So, we can model
this auction with the following function, which calculates a single
bidder’s utility:
let fixedprice b p = if b > p then v - p else 0

For clarity, we treat v as a parameter declared in context with
refinement type tv :: R | vŸ “ vŹ u. Truthfulness of this auction
follows from the type of fixedprice:
tb :: R | bŸ “ vu Ñ tp :: R | pŸ “ pŹ u Ñ tu :: R | uŸ ě uŹ u.
The relational variable b is required to be equal to v in the first run,
and arbitrary on the second run. Then, the final utility u cannot be
higher on the second run, demonstrating truthfulness.
This example also demonstrates a boolean version of the asynchronous typing rule AC ASE from Figure 5. Since the bid b is
arbitrary in the second run, the two runs may take different branches.
Indeed, these are the most interesting cases of the reasoning: If the
same branch is taken in both runs, then the utility is the same in
both runs (since the price is the same in both runs). When different
branches are taken, we verify that truthfulness holds even when
deviating from truthful bidding changes the outcome of the auction.
6.2

Since the mechanism is randomized, we want to verify truthfulness in expectation: an individual’s expected utility will never
increase if she deviates from bidding her true value. In fact, the
random sampling auction satisfies a stronger property, known as
universal truthfulness: a bidder will never be able to gain by deviating from truthful bidding, even knowing the random coins of the
mechanism.
To model the random sampling auction, we will treat as parameters the value v : R of the single deviating bidder ˚ and the bids of
the other bidders bs : R list; these are again assumed to the same
on both runs. We define a (deterministic) utility function that takes
the bid (b) for the deviating bidder ˚, a coin (mygrp) indicating the
group of ˚, and a list of coins (othergrp) indicating the groups of the
other bidders. Then, utility for ˚ is computed using the fixed-price
auction with reserve price from the bids in the other group; the
optimal reserve price function is denoted by optfixed:
let utility b (mygrp, othergrp) =
let (g1 , g2 ) =
split (mygrp :: othergrp) (b :: bs) in
if mygroup
then fixedprice b (optfixed g2 )
else fixedprice b (optfixed g1 )

Universal truthfulness can be seen from the type of utility:
tb :: R | bŸ “ vŸ u Ñ tc :: B ˆ B list | cŸ “ cŹ u
Ñ tu :: R | uŸ ě uŹ u
The type shows that for any realization of the randomness, the utility
is maximized by truthful reporting.
The main auction takes in the real-valued bid b of ˚, draws the
booleans indicating the groups, and uses the expectation operation
to compute the expected utility of ˚ on this distribution:
let auction b =
mlet me
= flip
in
mlet others = repeat N flip
in
let coins = munit (me, others) in
E coins (utility b)

Above, flip returns a uniformly random boolean, and has type
M0,0 rtc :: B | cŸ “ cŹ us.
The repeat function is used to generate a list of N random booleans
(where N ` 1 is the total number of bidders) that are then used to
split the other bidders into two groups.
Truthfulness for the random sampling auction is reflected by the
type for auction, which computes the expected utility of ˚:
tb :: R | bŸ “ vŸ u Ñ tu :: R | uŸ ě uŹ u.

Universal Truthfulness and Randomized Mechanisms

While the fixed-price auction is very simple, it has poor revenue
properties since the price is set independently of the bids. Setting it
too high will lead to very few goods sold (and hence low revenue),
and setting it too low may sell many goods, but at a price that is
substantially less than bidders would have been willing to pay (again,
low revenue). However, picking the price as a function of the bids
can destroy the auction’s truthfulness property. What to do?
It turns out that randomization is a useful way around this
problem. In the random sampling auction due to Goldberg et al.
[27], the bidders are randomly split into two groups g1 and g2 . The
fixed-price maximizing revenue is computed for each group, and
then a fixed-price auction is run in each group—but using the price
computed from the other group. Truthfulness holds since the price
charged to any bidder remains independent of her own bid.
4 While

it is possible to code the full auction that calculates all the winners
and charges all the prices, we verify the core guarantee of truthfulness, which
deals with a single bidder’s utility function.

To verify the truthfulness of this auction we rely on monotonicity of
expectation, as captured by the refinement type from § 2.
6.3

Nash Equilibrium via Differential Privacy

In this section, we move beyond auctions and consider the more
general setting of games. A game is played by a collection of N
agents indexed by i, each with a set of possible actions Ai (the
action space). Given a vector of actions (one for each player)
a “ pa1 , . . . , aN q, each agent receives a (possibly randomized)
payoff Pi pa1 , . . . , aN q; agents seek to maximize their (expected)
payoff. For an example, auctions can be considered as games where
each agent’s action space is the space of possible bids, and the payoff
of each agent is their utility for the chosen outcome.
So far, we have considered mechanisms where one action (truthfully reporting) is a dominant strategy: a maximum payoff strategy
no matter how the opponents play. In general games, like rock-paper
scissors, dominant strategies usually do not exist. In this section, we
consider a weaker solution concept: approximate Nash equilibrium.

let rec mkSums i br* br =
mlet s = lap (sign (br* i) (br i))
match i with
| 0
Ñ munit [s]
| i’ + 1 Ñ
mlet ss = mkSums i’ br* br
munit (s :: ss)

in

in

let rec search i br* br sums =
if |i - nth i sums| < T + 1/2
then i
else match i with
| 0
Ñ0
| i’ + 1 Ñ search i’ br* br sums
let expay br* dev* br dev =
E (mlet sums = mkSums k br* br
let
s‚
= search k br* br sums
let
a*
= dev* (br* s ‚ )
let
a
= dev (br s ‚ )
let
p*
= pay* a* (sign a* a)
munit p*) ( λ x. x)

deviating player, while the other agent is a meta-player, representing
all of the other players in the aggregative game (who do not deviate).
The relevant code for the mechanism is in Figure 10. The function expay computes the expected pay-off for bidder ˚; it takes as
inputs best response functions br* and br that map signals to an
agent’s highest payoff action (this is how agents report their payoff), and deviation functions dev* and dev that map recommended
actions to actual actions. Agents also have a true payoff, pay* and
pay, also considered as parameters since they are the same in both
runs. The mechanism will not use these functions in the code; they
are only referred to by the refinements.
The function expay performs the following steps:
1. Use mkSums to compute a noisy list sums of signals, using the
Laplace mechanism;

in
in
in
in
in

Figure 10: Aggregative game mechanism

2. compute a signal s‚ such that if both agents choose their (selfreported) best action br s‚ and br* s‚ for signal s‚ , then the true
signal based on strategy profiles a and a* (defined next) is close
to s‚ ;
3. apply the deviation functions dev and dev* to the recommended
action br s‚ and br* s‚ of each player to produce the strategy
profile a and a*;
4. calculate the true payoff p* for the deviating agent on the
strategy profile;
5. compute the expectation of the payoff p* for the deviating agent.

Definition 6.1. Let α ě 0. An assignment of agents to actions
(a strategy profile) pa1 , . . . , aN q is an α-approximate Nash equilibrium if no single agent i can gain more than α payoff from a
unilateral deviation from ai , assuming that all other players are
playing according to a. That is, for all agents i and actions a1i ,
ErPi pa1 , . . . , ai , . . . aN qs ě ErPi pa1 , . . . , a1i , . . . aN qs ´ α.
We consider an algorithm for computing an approximate Nash
equilibrium when the payoffs are not publicly known. There are
at least two difficulties: first, a general game may have several
Nash equilibria; agents may prefer different equilibria among the
many that exist. This may lead agents to misrepresent their payoff
functions to influence which equilibrium is selected, something we
want to prevent. Second, payoff functions may consist of sensitive
information, and agents may be unwilling to reveal their payoffs to
the mechanism if the output could disclose their private information.
Somewhat remarkably, using differential privacy to solve the
second problem also solves the first: if we can compute a Nash
equilibrium under differential privacy, then the profile of actions
when agents truthfully report their payoff function is an approximate
Nash equilibrium. A full discussion is beyond the scope of this paper;
we present and verify the approximate Nash equilibrium property
for a version of a mechanism due to Cummings et al. [13], which
computes approximate Nash equilibrium of aggregative games.
In an aggregative game, payoffs are a function only of an agent’s
own action and a signal, a non-negative real number bounded by k
that depends on the aggregated actions of all players. That is, the
payoff function for bidder i is of the form Pi pai , Spa1 , . . . , aN qq,
where S is a signal function of type A1 ˆ ¨ ¨ ¨ ˆ AN Ñ r0, ks.
In code, we will write sign for the signal function and k for the
bound; they are the same in both runs and we consider them implicit
parameters.
The mechanism we have verified computes an equilibrium of an
aggregative game, where the payoffs are reported by the agents. We
want to show that reporting the true payoff and playing the action
suggested by the mechanism is an approximate Nash equilibrium.
To keep the notation light, we think of all players as having the
same action space, and we consider only two players with actions
a* and a, respectively. We consider the player ˚ as the possibly

Players have two opportunities to deviate: they could misreport
their best response function, or they could choose a deviation
function to play differently than their recommendation. We want to
show that reporting the true best response function and following
the recommendation (i.e., using the identity function for deviation)
is an approximate Nash equilibrium. As before, we perform the
verification by assigning expay a relational refinement type where ˚
behaves truthfully in the left execution, while in the right execution
˚ behaves arbitrarily. Assuming that br*Ÿ is the true best response
function corresponding to pay*, and that dev*Ÿ is the identity
function, and that br and dev coincide on both runs (we thus omit
subscripts), we want to prove (according to Definition 6.1):
expay br*Ÿ devŸ br dev

ě

expay br*Ź dev*Ź br dev ´ α

for some value α. We do this by checking that expay has type:
Ñ
Ñ
Ñ
Ñ

tbr* :: R Ñ A
tdev* :: A Ñ A
tbr :: R Ñ A
tdev :: A Ñ A
`
tu
:: R

| @s, a. pay* pbr*Ÿ sq s ě pay* a su
| @x. dev*Ÿ x “ xu
| brŸ “ brŹ u
| @a. devŸ a “ devŹ a “ au
| uŸ ě uŹ ´ αu.

We briefly comment on the two most interesting steps in the
verification. First, when calculating s‚ , the algorithm computes
sums by adding Laplace noise to each induced best response: we
want to ensure that agents have a limited influence on the chosen
signal (and hence have limited incentive to misreport their best
response strategy). For the accuracy guarantee we need to show
that this noise is not too large (which is the case if the signal and
payoff functions satisfy certain low-sensitivity conditions captured
with refinement types). This is modeled by assigning to the Laplace
mechanism lap a refinement type capturing accuracy:
Πpx :: Rq. M|xŸ ´xŹ |,β rtu :: R | uŸ “ uŹ ^ |xŸ ´ uŸ | ă T us,
where T is defined as |xŸ ´ xŹ | ` 1 log β2 . Informally, this states
that the added noise is less than T with probability 1 ´ β.
The second interesting point is taking the expected value. The
expression payoff p* is randomized, and has type
M1 ,δ1 rtu :: R` | uŸ ě uŹ ´ α1 us

for some concrete values of 1 , δ 1 and α1 . The payoff above is
a probability distribution on real numbers, related by the lifted
inequality relation. We wish to take the expected value of these
distributions, in order to relate the expected payoff on the two runs.
However, a priori, it is not clear how the expected values of these
distributions are related. Fortunately, the expected values are related
in a rather simple way, as seen in the following refinement for E:
Ñ
Ñ

M1 ,δ1 rtx :: R` | xŸ ě xŹ ´ α1 us
tf :: R` Ñ R` | fŸ “ fŹ “ idu
`
tu :: R | uŸ ě uŹ ´ α2 u,

where α2 is an expression computed from 1 , δ 1 , and α1 . That is,
taking expectation of two distributions related by the lifted inequality
relation yields two real numbers that are approximately related by
the unlifted, standard inequality relation on real numbers. Though
not obvious, the soundness of this refinement can be derived from
the definition of expectation and lifting.
From this refinement on the expected payoff for ˚ computed
by expay, we conclude that truthful reporting and following the
recommended action is an approximate Nash equilibrium.

7.

Related Work

Our work lies at the intersection of differential privacy, mechanism
design, probabilistic programming languages, and verification. We
briefly comment on the first three areas (which are too enormous to
be covered here) and elaborate on the most relevant work in program
verification.
Differential privacy Differential privacy, first proposed by Blum
et al. [7] and formally defined by Dwork et al. [20], has been an
area of intensive research in the last decade. We have touched on a
handful of private algorithms, including an algorithm for computing
running sums [11] (part of a broader literature on streaming privacy),
answering large classes of queries [25] (part of a broader literature
on learning-theoretic approaches to data privacy). We refer readers
interested in a more comprehensive treatment to the excellent
surveys by Dwork [18, 19].
Mechanism Design Mechanism design was introduced to the theoretical computer science community (with a new focus on efficient
implementations) by the seminal work of Nisan and Ronen [41]; see
Nisan et al. [42] for a textbook introduction. It is understood that
truthfulness guarantees can be difficult to prove and verify, so there
is a literature giving generic reductions from mechanism design
to algorithm design in limited settings, but it is known that this is
not possible in full generality [2, 12, 16, 32]. Differential privacy
was first proposed as a tool in mechanism design by McSherry and
Talwar [38], and has since found many applications; see Pai and
Roth [44] for a survey of this area.
Probabilistic programs There is a long line of work that develops
models of probabilistic programs. The monadic representation of
distributions originates from Giry [26] and was further developed in
a programming language setting by later work [8, 34, 45, 47]. The
connections with machine learning have recently triggered a surge of
interest in probabilistic programming languages. We refer the reader
to recent introductory articles [28, 29] for further information.
Verification of higher-order programs The refinement type discipline was introduced by Freeman and Pfenning [23], and further
developed by others [14, 17, 55]. Advances in SMT solvers have allowed practical systems that support refinement types through SMT
back-ends, for instance F7 [5], F‹ [51], and L IQUID H ASKELL [49].
Our work is mostly related to a recent variant of F‹ called RF‹ [4].
Like HOARe2 , RF‹ supports relational reasoning of probabilistic
computations. However, RF‹ lacks support for approximate relational refinement types and higher-order refinements, which are

both critical for verifying differential privacy and game-theoretic
properties.
Dependent types is another expressive typing discipline that
can be used to verify properties of functional programs—they
also form the basis of proof assistants like Coq. Examples of
dependently typed languages include Cayenne [1], Epigram [36],
Idris [9] and Trellys [10]. Like our system, Trellys distinguishes
between terminating and non-terminating expressions to ensure
logical consistency.
Other prominent approaches for verifying functional programs
include dynamic checking [22] (and its combination with static
type-checking [30, 31, 54]), model-checking [43] and translating
functional programs into logic [53].
Verification of differential privacy and mechanism design There
has been significant work on language-based techniques for verifying differentially privacy. Pierce [46] defines three categories:
run-time enforcement (PINQ [37], A IRAVAT [50]), static enforcement (Fuzz [48], DFuzz [24]), and verification-based enforcement
(CertiPriv [3]). Our work clearly falls into the last category. All
these works are focused on privacy, rather than accuracy. See Barthe
et al. [3], Pierce [46] for a more detailed account of related work.
There has been comparatively little work on language-based
techniques for verifying mechanism design. Lapets et al. [35] give
an interesting approach, by presenting a programming language
for automatically verifying simple auction mechanisms. A key
component of the language is a type analysis to determine if an
algorithm is monotone; if bidders have a single real number as their
value (single-parameter domains), then truthfulness is equivalent to
a monotonicity property (e.g., see Mu’Alem and Nisan [40]). Their
language can be extended by means of user-defined primitives that
preserve monotonicity. The paper shows the use of the language for
verifying two simple auction examples, but it is unclear how this
approach scales to larger auctions.
Finally, Fang et al. [21] propose the use of program synthesis
for verifying truthfulness of auctions. Their approach reduces the
verification of auction to linear constraints that can be handled by an
SMT solver. In this respect, their approach is similar in spirit to ours.
However, the constraints they consider are linear and moreover their
technique applies to imperative programs. The extension to higher
order functions is not obvious.

8.

Future Directions

HOARe2 is an expressive system of relational refinement types that
captures differential privacy, game-theoretic properties and other
relational properties of probabilistic computations. An exciting direction for further work is to formally verify more complex mechanisms whose truthfulness guarantees are less standard. For example,
it would be interesting to verify mechanisms that are merely truthful
in expectation, for which universally truthful analogues do not exist
(e.g., Dobzinski and Dughmi [15]). Such mechanisms use randomization in a crucial way for their incentive properties, and in addition
to being interesting challenges for verification, are mechanism for
which truthfulness is non-obvious. We also intend to develop a nonrelational version of HOARe2 for reasoning about the accuracy of
probabilistic computations.
Acknowledgements We thank Zhiwei Steven Wu for good discussions and in particular for suggesting the aggregative games example. We also thank the anonymous reviewers for their close reading
and helpful comments. This research was supported by the European Community’s Seventh Framework grant #272487, MINECO
grant TIN2012-39391-C04-01 (StrongSoft), Madrid regional project
S2009TIC-1465 (PROMETIDOS), and NSF grant CNS-1065060.

References
[1] L. Augustsson. Cayenne – a language with dependent types. In
ACM SIGPLAN International Conference on Functional Programming
(ICFP), Baltimore, Maryland, pages 239–250, 1998.
[2] M.-F. Balcan, A. Blum, J. D. Hartline, and Y. Mansour. Reducing
mechanism design to algorithm design via machine learning. Journal
of Computer and System Sciences, 74(8):1245–1270, 2008.
[3] G. Barthe, B. Köpf, F. Olmedo, and S. Zanella-Béguelin. Probabilistic
relational reasoning for differential privacy. In ACM SIGPLAN–
SIGACT Symposium on Principles of Programming Languages (POPL),
Philadelphia, Pennsylvania, pages 97–110, 2012.
[4] G. Barthe, C. Fournet, B. Grégoire, P.-Y. Strub, N. Swamy, and
S. Zanella-Béguelin. Probabilistic relational verification for cryptographic implementations. In ACM SIGPLAN–SIGACT Symposium on
Principles of Programming Languages (POPL), San Diego, California,
pages 193–206, 2014.
[5] J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis.
Refinement types for secure implementations. In IEEE Computer
Security Foundations Symposium, Pittsburgh, Pennsylvania, 2008.
[6] N. Benton. Simple relational correctness proofs for static analyses and
program transformations. In ACM SIGPLAN–SIGACT Symposium on
Principles of Programming Languages (POPL), Venice, Italy, pages
14–25, 2004.
[7] A. Blum, C. Dwork, F. McSherry, and K. Nissim. Practical privacy: the
SuLQ framework. In ACM SIGACT–SIGMOD–SIGART Symposium on
Principles of Database Systems (PODS), Baltimore, Maryland, pages
128–138, 2005.
[8] J. Bornholt, T. Mytkowicz, and K. S. McK|inley. Uncertainxty: A firstorder type for uncertain data. In Asian Symposium on Programming
Languages and Systems (APLAS), Salt Lake City, Utah, 2014.
[9] E. Brady. Idris, a general-purpose dependently typed programming
language: Design and implementation. Journal of Functional Programming, 23(5):552–593, 2013.
[10] C. Casinghino, V. Sjöberg, and S. Weirich. Combining proofs and
programs in a dependently typed langauge. In ACM SIGPLAN–SIGACT
Symposium on Principles of Programming Languages (POPL), San
Diego, California, 2014.
[11] T.-H. H. Chan, E. Shi, and D. Song. Private and continual release of
statistics. ACM Transactions on Information and System Security, 14
(3):26, 2011.
[12] S. Chawla, N. Immorlica, and B. Lucier. On the limits of black-box
reductions in mechanism design. In ACM SIGACT Symposium on
Theory of Computing (STOC), New York, New York, 2012.
[13] R. Cummings, M. Kearns, A. Roth, and Z. S. Wu. Privacy and truthful
equilibrium selection for aggregative games. Technical report, 2014.
[14] R. Davies and F. Pfenning. Intersection types and computational
effects. In ACM SIGPLAN International Conference on Functional
Programming (ICFP), Montréal, Québec, pages 198–208, 2000.
[15] S. Dobzinski and S. Dughmi. On the power of randomization in
algorithmic mechanism design. In IEEE Symposium on Foundations
of Computer Science (FOCS), Atlanta, Georgia, pages 505–514.
[16] S. Dughmi and T. Roughgarden. Black-box randomized reductions in
algorithmic mechanism design. SIAM Journal on Computing, 43(1):
312–336, 2014.
[17] J. Dunfield and F. Pfenning. Tridirectional typechecking. In ACM
SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Venice, Italy, pages 281–292.
[18] C. Dwork. Differential privacy. In International Colloquium on
Automata, Languages and Programming (ICALP), Venice, Italy, pages
1–12, 2006.
[19] C. Dwork. Differential privacy: A survey of results. In Theory and
Applications of Models of Computation (TAMC), Xi’an, China, volume
4978 of LNCS, pages 1–19. Springer Berlin Heidelberg, 2008.
[20] C. Dwork, F. McSherry, K. Nissim, and A. Smith. Calibrating noise to
sensitivity in private data analysis. In IACR Theory of Cryptography
Conference (TCC), New York, New York, pages 265–284, 2006.

[21] Y. Fang, S. Chaudhuri, and M. Vardi. Computer-aided mechanism
design, 2014. Poster at POPL’14.
[22] R. B. Findler and M. Felleisen. Contracts for higher-order functions. In
ACM SIGPLAN International Conference on Functional Programming
(ICFP), Pittsburgh, Pennsylvania, pages 48–59, 2002.
[23] T. Freeman and F. Pfenning. Refinement types for ML. In ACM
SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, pages 268–277, 1991.
[24] M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce.
Linear dependent types for differential privacy. In ACM SIGPLAN–
SIGACT Symposium on Principles of Programming Languages (POPL),
Rome, Italy, pages 357–370, 2013.
[25] M. Gaboardi, E. J. Gallego Arias, J. Hsu, A. Roth, and Z. S. Wu. Dual
query: Practical private query release for high dimensional data. In
International Conference on Machine Learning (ICML), Beijing, China,
2014.
[26] M. Giry. A categorical approach to probability theory. Categorical
Aspects of Topology and Analysis, pages 68–85, 1982.
[27] A. V. Goldberg, J. D. Hartline, A. R. Karlin, M. Saks, and A. Wright.
Competitive auctions. Games and Economic Behavior, 55(2), 2006.
[28] N. D. Goodman. The principles and practice of probabilistic programming. In ACM SIGPLAN–SIGACT Symposium on Principles of
Programming Languages (POPL), Rome, Italy, pages 399–402, 2013.
[29] A. D. Gordon, T. A. Henzinger, A. V. Nori, and S. K. Rajamani.
Probabilistic programming. In International Conference on Software
Engineering (ICSE), Hyderabad, India, pages 167–181, 2014.
[30] M. Greenberg, B. C. Pierce, and S. Weirich. Contracts made manifest.
In ACM SIGPLAN–SIGACT Symposium on Principles of Programming
Languages (POPL), Madrid, Spain, pages 353–364, 2010.
[31] J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage:
Hybrid checking for flexible specifications. In Scheme and Functional
Programming Workshop, pages 93–104, 2006.
[32] J. D. Hartline and B. Lucier. Bayesian algorithmic mechanism design. In ACM SIGACT Symposium on Theory of Computing (STOC),
Cambridge, Massachusetts, pages 301–310, 2010.
[33] M. Hicks, G. Bierman, N. Guts, D. Leijen, and N. Swamy. Polymonadic
programming. In Workshop on the Mathematical Foundations of
Programming Semantics (MFPS), Ithaca, New York, 2014.
[34] O. Kiselyov and Chung-Chieh Shan. Embedded probabilistic programming. In DSL, pages 360–384, 2009.
[35] A. Lapets, A. Levin, and D. Parkes. A Typed Truthful Language
for One-dimensional Truthful Mechanism Design. Technical Report
BUCS-TR-2008–026, 2008.
[36] C. McBride. Epigram: Practical programming with dependent types. In
Advanced Functional Programming, pages 130–170. Springer, 2005.
[37] F. McSherry. Privacy integrated queries. In ACM SIGMOD International Conference on Management of Data (SIGMOD), Providence,
Rhode Island, 2009.
[38] F. McSherry and K. Talwar. Mechanism design via differential privacy.
In IEEE Symposium on Foundations of Computer Science (FOCS),
Providence, Rhode Island, pages 94–103, 2007.
[39] P. Milgrom and I. Segal. Deferred-acceptance auctions and radio
spectrum reallocation. In ACM SIGecom Conference on Economics
and Computation (EC), Palo Alto, California, pages 185–186, 2014.
[40] A. Mu’Alem and N. Nisan. Truthful approximation mechanisms for
restricted combinatorial auctions. Games and Economic Behavior, 64
(2):612–631, 2008.
[41] N. Nisan and A. Ronen. Algorithmic mechanism design. In ACM
SIGACT Symposium on Theory of Computing (STOC), Atlanta, Georgia,
pages 129–140, 1999.
[42] N. Nisan, T. Roughgarden, E. Tardos, and V. V. Vazirani. Algorithmic
game theory. Cambridge University Press, 2007.
[43] C.-H. L. Ong and S. J. Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In ACM SIGPLAN–
SIGACT Symposium on Principles of Programming Languages (POPL),
Austin, Texas, volume 46, pages 587–598, 2011.

[44] M. M. Pai and A. Roth. Privacy and mechanism design. ACM SIGecom
Exchanges, 12(1):8–29, 2013.
[45] S. Park, F. Pfenning, and S. Thrun. A probabilistic language based upon
sampling functions. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Long Beach, California,
pages 171–182, 2005.
[46] B. C. Pierce. Differential privacy in the programming languages
community, 2012. Invited tutorial at DIMACS Workshop on Recent
Work on Differential Privacy across Computer Science.
[47] N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads
of probability distributions. In ACM SIGPLAN–SIGACT Symposium
on Principles of Programming Languages (POPL), Portland, Oregon,
pages 154–165, 2002.
[48] J. Reed and B. C. Pierce. Distance makes the types grow stronger:
A calculus for differential privacy. In ACM SIGPLAN International
Conference on Functional Programming (ICFP), Baltimore, Maryland,
2010.
[49] P. M. Rondon, M. Kawaguci, and R. Jhala. Liquid types. In ACM
SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Tucson, Arizona, pages 159–169, 2008.
[50] I. Roy, S. Setty, A. Kilzer, V. Shmatikov, and E. Witchel. Airavat:
Security and privacy for MapReduce. In USENIX Symposium on
Networked Systems Design and Implementation (NDSI), San Jose,
California, 2010.
[51] N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang.
Secure distributed programming with value-dependent types. In
ACM SIGPLAN International Conference on Functional Programming
(ICFP), Tokyo, Japan, 2011.
[52] N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. Peyton Jones.
Refinement Types for Haskell. In ACM SIGPLAN International
Conference on Functional Programming (ICFP), Gothenburg, Sweden,
2014.
[53] D. Vytiniotis, S. Peyton Jones, K. Claessen, and D. Rosén. Halo:
Haskell to logic through denotational semantics. In ACM SIGPLAN–
SIGACT Symposium on Principles of Programming Languages (POPL),
Rome, Italy, 2013.
[54] P. Wadler and R. B. Findler. Well-typed programs can’t be blamed. In
European Symposium on Programming (ESOP), York, England, pages
1–16, 2009.
[55] H. Xi and F. Pfenning. Dependent types in practical programming. In
ACM SIGPLAN–SIGACT Symposium on Principles of Programming
Languages (POPL), San Antonio, Texas, pages 214–227, 1999.

