pith. sign in

arxiv: 2606.19686 · v1 · pith:PY3CPHPJnew · submitted 2026-06-18 · 💻 cs.PL

Effect Systems as Abstract Interpretations

Colin S. Gordon This is my paper

Pith reviewed 2026-06-26 15:37 UTC · model grok-4.3

classification 💻 cs.PL
keywords effect systemsabstract interpretationeffect quantalestype and effect systemsstatic analysisprogram semanticsabstract domains
0
0 comments X

The pith

Effect systems arise as abstract interpretations over event occurrences rather than states or values.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a formal connection between abstract interpretations and effect systems by embedding effect quantales into abstract domains. It further recovers the structure of an effect quantale itself as an abstract interpretation performed on event occurrences during program execution. This unifies two approaches to static reasoning about program behaviors that were previously connected only by loose hypotheses. A reader would care because it supplies a common semantic foundation for type-and-effect systems and abstract interpretation techniques. If the embedding holds, results and methods from one area transfer directly to the other.

Core claim

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.

What carries the argument

The embedding of effect quantales into abstract domains, which recovers effect systems as abstract interpretations performed on sequences of events.

If this is right

  • Properties proved for abstract interpretations transfer to the corresponding effect systems.
  • Effect systems inherit soundness and precision guarantees from the abstract interpretation framework.
  • The algebraic operations on effects correspond to the join and widening operations of the abstract domain.
  • Analyses based on effect systems can be re-expressed as event-sequence abstractions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Tool builders could implement effect tracking by reusing existing abstract interpretation engines that operate on event traces.
  • The event-based view suggests that effect systems might be composed or refined by changing the interpretation of observable events.
  • Similar embeddings could connect other static analyses, such as those for information flow, to abstract interpretation.

Load-bearing premise

A general class of effect systems can be captured using effect quantales as the underlying algebraic structure.

What would settle it

An effect system whose behavior cannot be represented by any effect quantale or whose embedding into an abstract domain fails to preserve the intended effect ordering or composition.

Figures

Figures reproduced from arXiv: 2606.19686 by Colin S. Gordon.

Figure 1
Figure 1. Figure 1: A simple effect language than repeating standard proofs, we will shortly develop type safety results using abstract interpretation. 2.2 Examples of Effect Systems Most readers are likely familiar with the most widely-used effect system: Java’s checked exceptions [27], where effects are the set of exceptions that may be thrown. Some are likely familiar with the modern twist of an effect system tracking whic… view at source ↗
Figure 2
Figure 2. Figure 2: Tate’s critical section effects as an effect quantale Crit. − represents an undefined result for composition. or uses the mutually-exclusive resource); and code which is insensitive to the critical section (𝜀). Note that repeated locking or unlocking is undefined, as is the join of effects corresponding to different locking behaviour — as with reg￾ular type systems, effect systems perform both the analysis… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 1 minor

Summary. The paper claims to develop a formal relationship between abstract interpretations and a general class of effect systems. It first describes an embedding of effect quantales into abstract domains, then recovers the general form of an effect quantale as an abstract interpretation on event occurrences (rather than states or values). The approach is positioned as addressing the unsettled status of type-and-effect systems as abstract interpretations.

Significance. If the embedding and recovery hold with proper Galois connections, the result would provide a unifying perspective that could transfer soundness and precision results between the two formalisms. This is a potentially significant contribution to static analysis, as it targets an area where relationships are infrequently formalized despite existing hypotheses in the literature.

minor comments (1)
  1. The abstract is high-level; the manuscript should include explicit definitions of the embedding (e.g., how effect quantale operations map to abstract domain operations) and the recovery construction to allow verification of the claimed Galois connections.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their summary of the manuscript and for noting its potential significance in unifying effect systems and abstract interpretations via Galois connections. The recommendation is listed as uncertain, but the report contains no specific major comments or points of criticism. We therefore have no individual referee comments to address point-by-point.

Circularity Check

0 steps flagged

No significant circularity: direct embedding between formalisms

full rationale

The paper presents an embedding of effect quantales into abstract domains followed by recovery of the quantale form as an abstract interpretation over event occurrences. This is a correspondence between two established structures (effect quantales and Galois connections) rather than a derivation that reduces to its own inputs. No self-definitional steps, fitted predictions, or load-bearing self-citations appear in the abstract or described claims. The relationship is constructed explicitly from the definitions of the two formalisms, making the result independent of any circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The abstract relies on the standard algebraic properties of effect quantales and abstract domains; no free parameters, invented entities, or ad-hoc axioms are mentioned.

axioms (2)
  • domain assumption Effect quantales form an algebraic structure suitable for modeling effects in programs
    Invoked to enable the embedding into abstract domains
  • standard math Abstract domains can represent approximations of program behaviors
    Background assumption for the interpretation framework

pith-pipeline@v0.9.1-grok · 5612 in / 1206 out tokens · 20595 ms · 2026-06-26T15:37:40.459726+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

63 extracted references · 16 canonical work pages

  1. [1]

    Jorge Almeida, Stuart Margolis, Benjamin Steinberg, and Mikhail Volkov. 2009. Representation theory of finite semigroups, semigroup radicals and formal language theory.Trans. Amer. Math. Soc.361, 3 (2009), 1429–1461

    2009

  2. [2]

    1999.Type and Effect Systems: Behaviours for Concurrency

    Torben Amtoft, Flemming Nielson, and Hanne Riis Nielson. 1999.Type and Effect Systems: Behaviours for Concurrency. Imperial College Press, London, UK

    1999

  3. [3]

    Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, and Tiark Rompf. 2021. Reachability types: tracking aliasing and separation in higher-order functional programs.Proceedings of the ACM on Programming Languages5, OOPSLA (2021), 1–32

    2021

  4. [4]

    Andrej Bauer and Matija Pretnar. 2014. An effect system for algebraic effects and handlers.Logical methods in computer science10 (2014)

    2014

  5. [5]

    Nick Benton and Peter Buchlovsky. 2007. Semantics of an Effect Analysis for Exceptions. InTLDI. doi:10.1145/1190315.1190320

    work page doi:10.1145/1190315.1190320 2007

  6. [6]

    Lars Birkedal and Mads Tofte. 2001. A constraint-based region infer- ence algorithm.Theoretical Computer Science258, 1 (2001), 299 – 392. doi:10.1016/S0304-3975(00)00025-6

    work page doi:10.1016/s0304-3975(00)00025-6 2001

  7. [7]

    Bocchino, Jr., Vikram S

    Robert L. Bocchino, Jr., Vikram S. Adve, Danny Dig, Sarita V. Adve, Stephen Heumann, Rakesh Komuravelli, Jeffrey Overbey, Patrick Sim- mons, Hyojin Sung, and Mohsen Vakilian. 2009. A Type and Effect Sys- tem for Deterministic Parallel Java. InOOPSLA. doi:10.1145/1640089. 1640097

    work page doi:10.1145/1640089 2009

  8. [8]

    Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. 2002. Own- ership Types for Safe Programming: Preventing Data Races and Dead- locks. InOOPSLA. doi:10.1145/582419.582440 3Full higher-order polymorphic types in the sense of System F lack classical set-theoretic interpretations [45, 46], so treating higher-order polymorphism would be yet another non-t...

    work page doi:10.1145/582419.582440 2002

  9. [9]

    Patrick Cousot. 1997. Types as abstract interpretations. InProceed- ings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 316–331

    1997

  10. [10]

    Patrick Cousot. 2024. Calculational design of [in] correctness trans- formational program logics by abstract interpretation.Proceedings of the ACM on Programming Languages8, POPL (2024), 175–208

    2024

  11. [11]

    Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. InProceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 269–282

    1979

  12. [12]

    Patrick Cousot and Radhia Cousot. 1992. Abstract interpretation frameworks.Journal of logic and computation2, 4 (1992), 511–547

    1992

  13. [13]

    Pierre-Évariste Dagand, Nicolas Tabareau, and É ric Tanter. 2018. Foun- dations of dependent interoperability.Journal of Functional Program- ming28 (2018), e9

    2018

  14. [14]

    Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang. 2013. Views: compositional reason- ing for concurrent programs. InProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages. 287–300

    2013

  15. [15]

    Cormac Flanagan and Martín Abadi. 1999. Object Types against Races. InCONCUR. doi:10.1007/3-540-48320-9_21

    work page doi:10.1007/3-540-48320-9_21 1999

  16. [16]

    Cormac Flanagan and Stephen N. Freund. 2000. Type-Based Race Detection for Java. InPLDI. doi:10.1145/349299.349328

    work page doi:10.1145/349299.349328 2000

  17. [17]

    Cormac Flanagan and Shaz Qadeer. 2003. A Type and Effect System for Atomicity. InProceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI ’03). ACM, 338–349. doi:10.1145/781131.781169

    work page doi:10.1145/781131.781169 2003

  18. [18]

    Cormac Flanagan and Shaz Qadeer. 2003. Types for Atomicity. In Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI ’03). ACM, 1–12. doi:10. 1145/604174.604176

    arXiv 2003

  19. [19]

    Gifford and John M

    David K. Gifford and John M. Lucassen. 1986. Integrating Functional and Imperative Programming. InProceedings of the 1986 ACM Con- ference on LISP and Functional Programming (LFP ’86). doi:10.1145/ 319838.319848

    arXiv 1986

  20. [20]

    Colin S Gordon. 2017. A Generic Approach to Flow-Sensitive Poly- morphic Effects. In31st European Conference on Object-Oriented Pro- gramming (ECOOP 2017)

    2017

  21. [21]

    Colin S Gordon. 2020. Lifting Sequential Effects to Control Operators. In34th European Conference on Object-Oriented Programming (ECOOP 2020)

    2020

  22. [22]

    Colin S. Gordon. 2021. Polymorphic Iterable Sequential Effect Systems. ACM Transactions on Programming Languages and Systems (TOPLAS) (2021)

    2021

  23. [23]

    Colin S Gordon, Werner Dietl, Michael D Ernst, and Dan Grossman

  24. [24]

    InEuropean Conference on Object-Oriented Programming

    JavaUI: effects for controlling UI object access. InEuropean Conference on Object-Oriented Programming. Springer, 179–204

  25. [25]

    Colin S Gordon, Michael D Ernst, and Dan Grossman. 2012. Static lock capabilities for deadlock freedom. InProceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation. 67–78

    2012

  26. [26]

    Colin S Gordon, Matthew J Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. 2012. Uniqueness and reference immutability for safe parallelism. InProceedings of the ACM international conference on Object oriented programming systems languages and applications. 21– 40

    2012

  27. [27]

    Colin S Gordon and Chaewon Yun. 2023. Error Localization for Se- quential Effect Systems. InInternational Static Analysis Symposium. Springer, 343–370

    2023

  28. [28]

    2014.The Java Language Specification: Java SE 8 Edition

    James Gosling, Bill Joy, Guy L Steele, Gilad Bracha, and Alex Buckley. 2014.The Java Language Specification: Java SE 8 Edition. Pearson Education

    2014

  29. [29]

    Martin Hofmann and Wei Chen. 2014. Abstract interpretation from Büchi automata. InProceedings of the Joint Meeting of the Twenty-Third Gordon EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–10

    2014

  30. [30]

    Stefan Holdermans and Jurriaan Hage. 2010. Polyvariant flow analysis with higher-ranked polymorphic types and higher-order effect opera- tors. InProceedings of the 15th ACM SIGPLAN international conference on Functional programming. 63–74

    2010

  31. [31]

    Andrej Ivašković and Alan Mycroft. 2020. A graded Monad for deadlock-free concurrency (functional pearl). InProceedings of the 13th ACM SIGPLAN International Symposium on Haskell. 17–30

    2020

  32. [32]

    Andrej Ivašković, Alan Mycroft, and Dominic Orchard. 2020. Data- Flow Analyses as Effects and Graded Monads. In5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). 15:1–15:23. doi:10.4230/LIPIcs.FSCD.2020.15

    work page doi:10.4230/lipics.fscd.2020.15 2020

  33. [33]

    Pierre Jouvelot and David Gifford. 1991. Algebraic reconstruction of types and effects. InProceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 303–310

    1991

  34. [34]

    Kevin Kappelmann. 2023. Transport via partial galois connections and equivalences. InAsian Symposium on Programming Languages and Systems. Springer, 225–245

    2023

  35. [35]

    Andrew J. Kennedy. 1996. Type Inference and Equational Theories. Technical Report LIX/RR/96/09, LIX(1996)

    1996

  36. [36]

    Eric Koskinen and Tachio Terauchi. 2014. Local Temporal Reasoning. InProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Vienna, Austria)(CSL-LICS ’14). ACM, New York, NY, USA, Article 59, 10 pages. doi:10.1145/26030...

    work page doi:10.1145/2603088.2603138 2014

  37. [37]

    D. Kozen. 1994. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events.Information and Computation110, 2 (1994), 366 – 390. doi:10.1006/inco.1994.1037

    work page doi:10.1006/inco.1994.1037 1994

  38. [38]

    Dexter Kozen. 1997. Kleene algebra with tests.ACM Transactions on Programming Languages and Systems (TOPLAS)19, 3 (1997), 427–443. doi:10.1145/256167.256195

    work page doi:10.1145/256167.256195 1997

  39. [39]

    J. M. Lucassen and D. K. Gifford. 1988. Polymorphic Effect Systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). doi:10.1145/73560.73564

    work page doi:10.1145/73560.73564 1988

  40. [40]

    Holbrook Mann MacNeille. 1937. Partially ordered sets.Trans. Amer. Math. Soc.42, 3 (1937), 416–460

    1937

  41. [41]

    Magnus Madsen, Jaco Van de Pol, and Troels Henriksen. 2023. Fast and efficient boolean unification for Hindley-Milner-style type and effect systems.Proceedings of the ACM on Programming Languages7, OOPSLA2 (2023), 516–543

    2023

  42. [42]

    Daniel Marino and Todd Millstein. 2009. A Generic Type-and-Effect System. InTLDI. doi:10.1145/1481861.1481868

    work page doi:10.1145/1481861.1481868 2009

  43. [43]

    Mihai Nicola, Chaitanya Agarwal, Eric Koskinen, and Thomas Wies

  44. [44]

    Abstract Interpretation of Temporal Safety Effects of Higher Order Programs.Proceedings of the ACM on Programming Languages 9, OOPSLA2 (2025), 2511–2539

    2025

  45. [45]

    Flemming Nielson and Hanne Riis Nielson. 1993. From CML to process algebras. InInternational Conference on Concurrency Theory (CONCUR). Springer, 493–508. doi:10.1007/3-540-57208-2_34

    work page doi:10.1007/3-540-57208-2_34 1993

  46. [46]

    Flemming Nielson and Hanne Riis Nielson. 1994. Constraints for polymorphic behaviours of concurrent ML. InInternational Conference on Constraints in Computational Logics. Springer, 73–88

    1994

  47. [47]

    Andrew M Pitts. 1987. Polymorphism is set theoretic, constructively. InCategory Theory and Computer Science: Edinburgh, UK, September 7–9, 1987 Proceedings. Springer, 12–39

    1987

  48. [48]

    John C Reynolds. 1984. Polymorphism is not set-theoretic. InInterna- tional Symposium on Semantics of Data Types. Springer, 145–156

    1984

  49. [49]

    Hannes Saffrich and Peter Thiemann. 2022. Relating functional and imperative session types.Logical Methods in Computer Science18 (2022)

    2022

  50. [50]

    David A Schmidt. 2012. Inverse-limit and topological aspects of ab- stract interpretation.Theoretical Computer Science430 (2012), 23–42

    2012

  51. [51]

    Taro Sekiyama and Hiroshi Unno. 2023. Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations.Proceedings of the ACM on Programming Languages7, POPL (2023), 2079–2110

    2023

  52. [52]

    Taro Sekiyama and Hiroshi Unno. 2025. Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs. Proceedings of the ACM on Programming Languages9, POPL (2025), 2306–2336

    2025

  53. [53]

    Christian Skalka. 2008. Types and trace effects for object orientation. Higher-Order and Symbolic Computation21, 3 (2008), 239–282. doi:10. 1007/s10990-008-9032-6

    2008

  54. [54]

    Christian Skalka, David Darais, Trent Jaeger, and Frank Capobianco

  55. [55]

    In2020 IEEE 33rd Computer Security Foundations Symposium (CSF)

    Types and abstract interpretation for authorization hook advice. In2020 IEEE 33rd Computer Security Foundations Symposium (CSF). IEEE, 139–152

  56. [56]

    Christian Skalka, Scott Smith, and David Van Horn. 2008. Types and trace effects of higher order programs.Journal of Functional Programming18, 2 (2008)

    2008

  57. [57]

    Kohei Suenaga. 2008. Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references. InAsian Symposium on Programming Languages and Systems. Springer, 155–

    2008

  58. [58]

    doi:10.1007/978-3-540-89330-1_12

    work page doi:10.1007/978-3-540-89330-1_12

  59. [59]

    Yan Mei Tang and Pierre Jouvelot. 1994. Separate abstract inter- pretation for control-flow analysis. InInternational Symposium on Theoretical Aspects of Computer Software. Springer, 224–243

    1994

  60. [60]

    Ross Tate. 2013. The Sequential Semantics of Producer Effect Systems. InPOPL ’13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages. ACM. doi:10. 1145/2429069.2429074

    arXiv 2013

  61. [61]

    Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal

  62. [62]

    ACM71, 6 (2024), 1–75

    A logical approach to type soundness.J. ACM71, 6 (2024), 1–75

    2024

  63. [63]

    Marko van Dooren and Eric Steegmans. 2005. Combining the Ro- bustness of Checked Exceptions with the Flexibility of Unchecked Exceptions Using Anchored Exception Declarations. InProceedings of the 20th Annual ACM SIGPLAN Conference on Object-oriented Pro- gramming, Systems, Languages, and Applications (OOPSLA ’05). ACM, 455–471. doi:10.1145/1094811.1094847

    work page doi:10.1145/1094811.1094847 2005