Effect Systems as Abstract Interpretations

Gordon, Colin S.

International Workshop on Numerical and Symbolic Abstract Domains (NSAD), October 2026, doi: 10.1145/3840563.3843706

pdf slides doi

Abstract

Many forms of static reasoning about program behaviours are known in the literature, yet formal relationships are studied surprisingly infrequently. While most type systems are well-known to be captured by abstract interpretations, the situation for type-and-effect systems is, in the general case, unsettled despite strong hypotheses and occasional framing of effect systems as abstract interpretations. We develop a formal relationship between abstract interpretations and a general class of effect systems. First, we describe an embedding of effect quantales into abstract domains. Second, we recover the general form of an effect quantale as an abstract interpretation — not on states or values, but on event occurrences.

Bibtex

@inproceedings{nsad26,
	title = {Effect Systems as Abstract Interpretations},
	author = {Gordon, Colin S.},
	year = {2026},
	month = {October},
	booktitle = {International Workshop on Numerical and Symbolic Abstract
	             Domains (NSAD)},
	address = {Oakland, CA, USA},
        doi = {10.1145/3840563.3843706},
	abstract = {Many forms of static reasoning about program behaviours are
	            known in the literature, yet formal relationships are studied
	            surprisingly infrequently. While most type systems are well-known
	            to be captured by abstract interpretations, the situation for
	            type-and-effect systems is, in the general case, unsettled
	            despite strong hypotheses and occasional framing of effect
	            systems as abstract interpretations. We develop a formal
	            relationship between abstract interpretations and a general class
	            of effect systems. First, we describe an embedding of effect
	            quantales into abstract domains. Second, we recover the general
	            form of an effect quantale as an abstract interpretation — not on
	            states or values, but on event occurrences. },
}