Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Sun 18 Aug 2019 17:30 - 17:50 at Aurora Borealis - Effects Chair(s): David Darais

Dependently-typed languages are great for stating and proving properties of pure functions. We can reason about them modularly (state and prove their properties independently of other functions) and non-intrusively (without modifying their implementation). But what if we are interested in properties about the results of effectful computations? Ideally, we could keep on stating and proving them just as nicely.

This pearl shows we can. We formalise a way to lift a property about values to a property about effectful computations producing such values, and we demonstrate that we need not make any sacrifices when reasoning about them. In addition to this modular and non-intrusive reasoning, our approach offers independence of the underlying monad and allows for readable proofs whose structure follows that of the code.

Sun 18 Aug

tyde-2019-papers
17:10 - 18:10: TyDe 2019 - Effects at Aurora Borealis
Chair(s): David DaraisUniversity of Vermont
tyde-2019-papers17:10 - 17:30
Talk
Joris CeulemansKU Leuven, Andreas NuytsKU Leuven, Belgium, Dominique DevrieseVrije Universiteit Brussel
Pre-print
tyde-2019-papers17:30 - 17:50
Talk
Koen JacobsKU Leuven, Andreas NuytsKU Leuven, Belgium, Dominique DevrieseVrije Universiteit Brussel
Link to publication