Effectful Software Contracts

Cameron Moy, Christos Dimoulas, Matthias Felleisen

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Article number88
JournalProceedings of the ACM on Programming Languages
Issue numberPOPL
StatePublished - Jan 5 2024
Externally publishedYes


  • effect handlers
  • software contracts

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality


Dive into the research topics of 'Effectful Software Contracts'. Together they form a unique fingerprint.

Cite this