Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory

Overview

This work addresses modular verification in dependent type theory by formalizing Hoare's abstraction function methodology within univalent type theory. The paper proposes an encoding of abstraction functions as types themselves, establishing a linguistic framework that enforces the separation between concrete implementations and abstract specifications while preserving modularity guarantees essential for library-based software development.

Methods and approach

The approach employs a phase distinction mechanism that constructs a gluing structure, rendering abstraction functions as types and introducing a pair of modalities to decompose types into concrete and abstract components. A noninterference theorem characterizes the modularity guarantees arising from this phase distinction. The framework extends to cost analysis through a monadic sealing effect that enables cost-aware specifications, permitting implementations to be upper-bounded by their specifications even when private implementation details affect observable cost.

Results

The theory supports modular verification of both program behavior and cost within dependent type theory without requiring external methodological conventions. The gluing construction provides a type-theoretic foundation for Hoare's abstraction function methodology, with the noninterference theorem formalizing the privacy guarantees that prevent client code from observing or depending on implementation details. The extension to cost analysis demonstrates that the framework scales to resource-bounded verification, with the monadic sealing effect enabling precise cost specifications even in cases where private implementation details influence observable cost.

Implications

This work establishes a formal foundation for library-based program verification that enforces abstraction boundaries through type-theoretic structure rather than convention. By embedding abstraction functions as types, the approach provides machine-checkable guarantees that implementation-specific details do not leak into client reasoning, reducing the gap between specification and verification methodology. The cost-aware extension enables precise analysis of program cost relative to abstract specifications, supporting development of efficiency-conscious libraries where private details can be hidden while maintaining provable bounds on observable behavior.