Abstract
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.
| Original language | English |
|---|---|
| Article number | 113 |
| Pages (from-to) | 927 - 955 |
| Number of pages | 29 |
| Journal | Proceedings of the ACM on Programming Languages |
| Volume | 9 |
| Issue number | OOPSLA1 |
| DOIs | |
| Publication status | Published - 9 Apr 2025 |
| Event | ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH), OOPSLA track - Marina Bay Sands Convention Centre, Singapore, Singapore Duration: 12 Oct 2025 → 18 Oct 2025 https://2025.splashcon.org/track/OOPSLA |
Bibliographical note
Publisher Copyright:© 2025 Copyright held by the owner/author(s).
Research Groups and Themes
- Programming Languages