## Bidirectional proof refinement

In my last blog post, we looked at the very basics of proof refinement systems. I noted at the end that there was a big drawback of the systems as shown, namely that information flows only in one direction: from the root of a proof tree to the leaves. In this post, we’ll see how to get information to flow in the opposite direction as well.

The code for this blog post can be found on GitHub here.

### Addition Again

The addition judgment `Plus`

which we defined last time was a three-argument judgment. The judgment `Plus L M N`

was a claim that `N`

is the sum of `L`

and `M`

. But we might want to instead think about specifying only some of the arguments to this judgment. In a language like Prolog, this is implemented by the use of metavariables which get valued in the course of computation. In the proof refinement setting, however, we take a different approach. Instead, we make use of a notion called bidirectionality, where... Read more »