Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
2026-08-10 • Programming Languages
Programming LanguagesLogic in Computer Science
AI summaryⓘ
The authors introduce a new way to understand programs called operator semantics, which focuses on the building blocks (operators) behind fixed points in program behavior. They explain how abstract compilation can be seen as simplifying these operators. Their work develops advanced tools to analyze functions and programs using these operators, emphasizing how combining them works. They apply this framework to analyze the costs of recursive programs, creating methods that extract cost patterns independently of the solver used and work with complex data types and metrics.
least fixpointsoperator semanticsabstract compilationhigher-order abstract domainsrecurrence relationsstatic cost analysisrecursive programsalgebraic data typescatamorphismsprogram semantics
Authors
Louis Rustenholz, Alessio Mansutti, Pedro López-García, Félix Ridoux, Niki Vazou, Manuel V. Hermenegildo
Abstract
Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate representation between syntax and classical denotational semantics, which treats programs as operators. Abstract compilation is then understood as the act of abstracting such operators. We develop higher-order abstract domains for functions, operators, and programs themselves, in which composition is the key novel primitive, together with a categorical framework for constructing sound, precise, and modular abstract compilers. We instantiate this framework in the context of recurrence-based static cost analysis, developing solver-independent, optimal recurrence extraction techniques for recursive programs over algebraic data types, that support general function unknowns and catamorphic metrics, a broad class of size metrics beyond traditional approaches.