Unicorn is an online, in-memory social graph-aware indexing system designed to search trillions of edges between tens of billions of users and entities on thousands of commodity servers. Unicorn is based on standard concepts in information retrieval, but it includes features to promote results with good social proximity. It also supports queries that require multiple round-trips to leaves in order to retrieve objects that are more than one edge away from source nodes. Unicorn is designed to answer billions of queries per day at latencies in the hundreds of milliseconds, and it serves as an infrastructural building block for Facebook's Graph Search product. In this paper, we describe the data model and query language supported by Unicorn. We also describe its evolution as it became the primary backend for Facebook's search offerings.

This paper presents a new bisimulation theory for parametric polymorphism which enables straight forward co-inductive proofs of program equivalences involving existential types. The theory is an instance of typed normal form bisimulation and demonstrates the power of this recent framework for modeling typed lambda calculi as labelled transition systems.We develop our theory for a continuation-passing style calculus, Jump-With-Argument, where normal form bisimulation takes a simple form. We equip the calculus with both existential and recursive types. An "ultimate pattern matching theorem" enables us to define bisimilarity and we show it to be a congruence. We apply our theory to proving program equivalences, type isomorphisms and genericity.

Bohm tree equivalence up to possibly infinite eta expansion for the pure lambda-calculus can be characterized as a bisimulation equivalence. We call this co-inductive syntactic theory extensional head normal form bisimilarity and in this paper we extend it to the lambdaFP-calculus (the lambda-calculus with functional and surjective pairing) and to two untyped variants of Parigot's lambdamu-calculus. We relate the extensional head normal form bisimulation theories for the different calculi via Fujita's extensional CPS transform into the lambdaFP-calculus. We prove that extensional hnf bisimilarity is fully abstract for the pure lambda-calculus by a co-inductive reformulation of Barendregt's proof for Bohm tree equivalence up to possibly infinite eta expansion. The proof uses the so-called Bohm-out technique from Bohm's proof of the separation property for the lambda-calculus. Moreover, we extend the full abstraction result to extensional hnf bisimilarity for the lambdaFP-calculus. For the "standard" lambdamu-calculus, the separation property fails, as shown by David and Py, and for the same reason extensional hnf bisimilarity is not fully abstract. However, an "extended" variant of the lambdamu-calculus satisfies the separation property, as shown by Saurin, and we show that extensional hnf bisimilarity is fully abstract for this extended lambdamu-calculus

This paper describes two new bisimulation equivalences for the pure untyped call-by-value /spl lambda/-calculus, called enf bisimilarity and enf bisimilarity up to /spl eta/. They are based on eager reduction of terms to eager normal form (enf), analogously to co-inductive bisimulation characterizations of Levy-Longo tree equivalence and Bohm tree equivalence (up to /spl eta/). We argue that enf bisimilarity is the call-by-value analogue of Levy-Longo tree equivalence. Enf bisimilarity (up to /spl eta/) is the congruence on source terms induced by the call-by-value CPS transform and Bohm tree equivalence (up to /spl eta/) on target terms. Enf bisimilarity and enf bisimilarity up to /spl eta/ enjoy powerful bisimulation proof principles which, among other things, can be used to establish a retraction theorem for the call-by-value CPS transform.

We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus. Our first two results are theorems asserting the equivalence of our substitution-based semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.

This paper develops the functional part of a theory of action semantics for reasoning about programs. Action notation, the specification language of action semantics, is given an evaluation semantics, and operational techniques from process theory and functional programming are applied in the development of a versatile action theory. The power of the theory is demonstrated by means of action semantic proofs of functional program equivalences.