A Categorical Framework for Program Semantics and Semantic Abstraction
Shin-ya Katsumata, Xavier Rival, Jérémy Dubut
TL;DR
The paper develops a unified, category-theoretic framework for abstract interpretation by treating program semantics as oplax functors into the poset category and using lax natural transformations as concretizations. It separates collecting semantics into a denotational component and a property component via a functor C, enabling a functorial collecting semantics that supports monadic effectfulness and higher-order languages. Abstract interpretation is then systematically derived through Galois connections, yielding best abstract transformers and a category of abstractions, with constructive methods for finite-height domains and fixpoint over-approximation. The approach is demonstrated for both imperative languages (including while with variables) and the simply typed lambda calculus, yielding inductively definable abstract semantics and a robust pathway to practical static analysis. The framework promises broad applicability to other language families and fibrational setups, offering a principled avenue to integrate abstraction into categorical semantics and monadic effects.
Abstract
Categorical semantics of type theories are often characterized as structure-preserving functors. This is because in category theory both the syntax and the domain of interpretation are uniformly treated as structured categories, so that we can express interpretations as structure-preserving functors between them. This mathematical characterization of semantics makes it convenient to manipulate and to reason about relationships between interpretations. Motivated by this success of functorial semantics, we address the question of finding a functorial analogue in abstract interpretation, a general framework for comparing semantics, so that we can bring similar benefits of functorial semantics to semantic abstractions used in abstract interpretation. Major differences concern the notion of interpretation that is being considered. Indeed, conventional semantics are value-based whereas abstract interpretation typically deals with more complex properties. In this paper, we propose a functorial approach to abstract interpretation and study associated fundamental concepts therein. In our approach, interpretations are expressed as oplax functors in the category of posets, and abstraction relations between interpretations are expressed as lax natural transformations representing concretizations. We present examples of these formal concepts from monadic semantics of programming languages and discuss soundness.