Abstraction Functions as Types

Software development depends on the use of libraries whose specifications constrain the client's code and impose obligations on the implementation. It follows that any approach to verification at scale must also be modular, while permitting specification of both behavior and cost. Hoare's influential notion of an abstraction function provides an elegant and effective methodology for such verifications, separating the implementation from the specification, and using an abstraction function to demonstrate the behavioral correctness of the former relative to the latter. For all of its influence, much of the Hoare methodology relies on conventional separation between implementation and specification, providing no linguistic support for ensuring that these conventions are obeyed. The purpose of this paper is to propose a synthetic account of Hoare's methodology within univalent dependent type theory based on the principle that all types have abstract and concrete aspects by regarding abstraction functions as types. Achieving this relies crucially on the notion of a phase distinction in type theory, which gives rise to modalities that fracture a type into its concrete and abstract parts and that permit the definition of a type given these aspects using a technique called gluing. A noninterference theorem governing the phase distinction characterizes the modularity guarantees provided by the theory. Moreover, this approach scales to permit the specification and verification of the cost of programs, allowing clients to verify their own cost relative to a specification and permitting the implementation to be upper-bounded by the specification using a monadic sealing effect. The resulting theory supports modular development of programs and proofs in a manner that hides private details of no concern to clients while permitting precise specifications of both the cost and behavior of programs.