  Functional programs typically interact with stateful libraries that hide
state behind typed abstractions. One particularly important class of
applications are data structure implementations that rely on such libraries to
provide a level of efficiency and scalability that may be otherwise difficult
to achieve. However, because the specifications of the methods provided by
these libraries are necessarily general and rarely specialized to the needs of
any specific client, any required application-level invariants must often be
expressed in terms of additional constraints on the (often) opaque state
maintained by the library. In this paper, we consider the specification and
verification of such representation invariants using symbolic finite automata
(SFA). We show that SFAs can be used to succinctly and precisely capture
fine-grained temporal and data-dependent histories of interactions between
functional clients and stateful libraries. To facilitate modular and
compositional reasoning, we integrate SFAs into a refinement type system to
qualify stateful computations resulting from such interactions. The particular
instantiation we consider, Hoare Automata Types (HATs), allows us to both
specify and automatically type-check the representation invariants of a
datatype, even when its implementation depends on stateful library methods that
operate over hidden state. We also develop a new bidirectional type checking
algorithm that implements an efficient subtyping inclusion check over HATs,
enabling their translation into a form amenable for SMT-based automated
verification. We present extensive experimental results on an implementation of
this algorithm that demonstrates the feasibility of type-checking complex and
sophisticated HAT-specified OCaml data structure implementations.
