Effectful Software Contracts

Cameron Moy; Christos Dimoulas; Matthias Felleisen

doi:10.1145/3632930

Effectful Software Contracts

Cameron Moy, Christos Dimoulas, Matthias Felleisen

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English (US)
Article number	88
Journal	Proceedings of the ACM on Programming Languages
Volume	8
Issue number	POPL
DOIs	https://doi.org/10.1145/3632930
State	Published - Jan 5 2024

Keywords

effect handlers
software contracts

ASJC Scopus subject areas

Software
Safety, Risk, Reliability and Quality

Access to Document

10.1145/3632930

Cite this

@article{b0f27f3931ab4cfd9d139a255e9d55ca,

title = "Effectful Software Contracts",

abstract = "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.",

keywords = "effect handlers, software contracts",

author = "Cameron Moy and Christos Dimoulas and Matthias Felleisen",

note = "Publisher Copyright: {\textcopyright} 2024 Owner/Author.",

year = "2024",

month = jan,

day = "5",

doi = "10.1145/3632930",

language = "English (US)",

volume = "8",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "POPL",

}

TY - JOUR

T1 - Effectful Software Contracts

AU - Moy, Cameron

AU - Dimoulas, Christos

AU - Felleisen, Matthias

PY - 2024/1/5

Y1 - 2024/1/5

N2 - 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.

AB - 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.

KW - effect handlers

KW - software contracts

UR - http://www.scopus.com/inward/record.url?scp=85183076881&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85183076881&partnerID=8YFLogxK

U2 - 10.1145/3632930

DO - 10.1145/3632930

M3 - Article

AN - SCOPUS:85183076881

SN - 2475-1421

VL - 8

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 88

ER -

Effectful Software Contracts

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this