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.

@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}, note = {To Appear..}, 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. }, }