Scalability using effects

TL;DR

This paper explores leveraging computational effects to enhance scalability in specifications, demonstrating that effect-based specifications can be reasoned about without explicitly including the effects in the deduction system.

Contribution

It introduces a method to design deduction systems for effect-involving specifications without explicitly modeling the effects, improving scalability and correctness.

Findings

Effect-based specifications become more complex but more correct.

Deduction systems can handle effects implicitly.

The approach is demonstrated through two fundamental examples.

Abstract

This note is about using computational effects for scalability. With this method, the specification gets more and more complex while its semantics gets more and more correct. We show, from two fundamental examples, that it is possible to design a deduction system for a specification involving an effect without expliciting this effect.