How to do proofs? Practically proving properties about effectful programs' results (functional pearl)
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 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
17:10 - 18:10
|Reasoning about Effect Parametricity Using Dependent Types|
Joris Ceulemans KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit BrusselPre-print
|How to do proofs? Practically proving properties about effectful programs' results (functional pearl)|
Koen Jacobs KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit BrusselLink to publication