This paper proves an adequacy theorem for a general class of algebraic effects, including infinitary ones. The theorem targets a version of Call-by-Push-Value (CBPV), so that it applies to many possible evaluation mechanisms, including call-by-value. The calculus is given an operational semantics based on interaction trees, as well as a denotational semantics based on monad algebras. The main result, viz. that denotational equivalence implies observational equivalence, using a traditional logical relations argument.

@article{paperbot3177,
  title = {Adequacy for Algebraic Effects Revisited},
  author = {G. A. Kavvos},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA1},
  year = {2025},
  doi = {10.1145/3720457}
}