Secure computation allows multiple parties to
compute joint functions over private data
without leaking any sensitive data, typically
using powerful cryptographic
techniques. Writing secure applications using
these techniques directly can be challenging,
resulting in the development of several
programming languages and compilers that aim
to make secure computation
accessible. Unfortunately, many of these
languages either lack or have limited support
for rich recursive data structures, like
trees. In this paper, we propose a novel
representation of structured data types, which
we call oblivious algebraic data types, and a
language for writing secure computations using
them. This language combines dependent types
with constructs for oblivious computation, and
provides a security-type system which ensures
that adversaries can learn nothing more than
the result of a computation. Using this
language, authors can write a single function
over private data, and then easily build an
equivalent secure computation according to a
desired public view of their data.
