Functional programs typically interact with stateful libraries that hide state behind typed abstractions. 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. This paper addresses the specification and verification of such invariants using symbolic finite automata (SFA), which succinctly capture temporal and data-dependent histories of client-library interactions. To enable modular reasoning, we integrate SFAs into a refinement type system, qualifying stateful computations. Our approach, Hoare Automata Types (HATs), facilitates the specification and automatic type-checking of datatype invariants, even when implementations rely on stateful library methods with hidden state.

Zhe ZHOU（周喆） is currently a Ph.D. candidate in Computer Science at Purdue University, advised by Prof. Suresh Jagannathan and working closely with Prof. Benjamin Delaware. He earned his bachelor's degree from Peking University in 2017, where he was advised by Prof. Guangyu Sun. His research interests include programming languages (PL), particularly program verification and synthesis, property-based testing, and refinement types.