A predicate transformer semantics for effects: Functional Pearl

W.S. Swierstra, Tim Baanen

Research output: Contribution to journalArticleAcademicpeer-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 languageEnglish
Article number103
Number of pages26
JournalProceedings of the ACM on Programming Languages (PACM PL)
Volume3
Issue numberICFP
DOIs
Publication statusPublished - 2019

Keywords

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

Fingerprint

Dive into the research topics of 'A predicate transformer semantics for effects: Functional Pearl'. Together they form a unique fingerprint.

Cite this