How to Do Proofs: Practically Proving Properties About Effectful Programs39; Results (Functional Pearl)

Koen Jacobs, Andreas Nuyts, Dominique Devriese

Research output: Chapter in Book/Report/Conference proceedingConference paper

125 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationProceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development
Place of PublicationNew York, NY, USA
Number of pages13
ISBN (Electronic)9781450368155
ISBN (Print)978-1-4503-6815-5
Publication statusPublished - 18 Aug 2019
EventWorkshop on Type-Driven Development - Berlin, Germany
Duration: 18 Aug 201923 Aug 2019

Publication series

NameTyDe 2019


WorkshopWorkshop on Type-Driven Development
Abbreviated titleTyDe
Internet address


  • Agda
  • applicative
  • dependently-typed programming
  • effectful
  • equational reasoning
  • extrinsic proofs
  • functor
  • monad
  • strong specification

Cite this