A predicate transformer semantics for effects: Functional Pearl

W.S. Swierstra; Tim Baanen

doi:10.1145/3341707

A predicate transformer semantics for effects: Functional Pearl

W.S. Swierstra, Tim Baanen

Sub Software Technology

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

Abstract

Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.

Original language	English
Article number	103
Number of pages	26
Journal	Proceedings of the ACM on Programming Languages (PACM PL)
Volume	3
Issue number	ICFP
DOIs	https://doi.org/10.1145/3341707
Publication status	Published - 2019

Keywords

predicate transformers
effects
refinement
program calculation
weakestprecondition semantics
programming with dependent types
free monads
Agda

Access to Document

10.1145/3341707

3341707Final published version, 366 KB

Cite this

@article{3fe6cb9efd6b4c71b6dc711bab9abb17,

title = "A predicate transformer semantics for effects: Functional Pearl",

abstract = "Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.",

keywords = "predicate transformers, effects, refinement, program calculation, weakestprecondition semantics, programming with dependent types, free monads, Agda",

author = "W.S. Swierstra and Tim Baanen",

year = "2019",

doi = "10.1145/3341707",

language = "English",

volume = "3",

journal = "Proceedings of the ACM on Programming Languages (PACM PL)",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "ICFP",

}

TY - JOUR

T1 - A predicate transformer semantics for effects

T2 - Functional Pearl

AU - Swierstra, W.S.

AU - Baanen, Tim

PY - 2019

Y1 - 2019

N2 - Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.

AB - Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.

KW - predicate transformers

KW - effects

KW - refinement

KW - program calculation

KW - weakestprecondition semantics

KW - programming with dependent types

KW - free monads

KW - Agda

U2 - 10.1145/3341707

DO - 10.1145/3341707

M3 - Article

SN - 2475-1421

VL - 3

JO - Proceedings of the ACM on Programming Languages (PACM PL)

JF - Proceedings of the ACM on Programming Languages (PACM PL)

IS - ICFP

M1 - 103

ER -

A predicate transformer semantics for effects: Functional Pearl

Abstract

Keywords

Access to Document

Fingerprint

Cite this