Software contracts empower programmers to describe functional properties of components. When it comes to constraining effects, though, the literature offers only one-off solutions for various effects. It lacks a universal principle. This paper presents the design of an effectful contract system in the context of effect handlers. A key metatheorem shows that contracts cannot unduly interfere with a program’s execution. An implementation of this design, along with an evaluation of its generality, demonstrates that the theory can guide practice.

@article{paperbot2638,
  title = {Effectful Software Contracts},
  author = {Cameron Moy and Christos Dimoulas and Matthias Felleisen},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {POPL},
  year = {2024},
  doi = {10.1145/3632930}
}