ICFP 2019 (series) / Research Papers /
A predicate transformer semantics for effects (Functional Pearl)
Rasoning 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.
Wed 21 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Wed 21 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | Program VerificationResearch Papers at Aurora Borealis Chair(s): Adam Chlipala Massachusetts Institute of Technology | ||
10:30 22mTalk | A predicate transformer semantics for effects (Functional Pearl) Research Papers | ||
10:52 22mTalk | Dijkstra Monads for All Research Papers Kenji Maillard Inria Paris and ENS Paris, Danel Ahman University of Ljubljana, Robert Atkey University of Strathclyde, Guido Martínez CIFASIS-CONICET, Argentina, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Éric Tanter University of Chile & Inria Paris Pre-print | ||
11:15 22mTalk | Mechanized Relational Verification of Concurrent Programs with Continuations Research Papers | ||
11:37 22mTalk | Sequential Programming for Replicated Data Stores Research Papers Nicholas V. Lewchenko University of Colorado Boulder, Arjun Radhakrishna Microsoft, Akash Gaonkar , Pavol Cerny University of Colorado Boulder DOI Pre-print | ||