In the third post in this series (part 1, part 2) on proof refinement, I'm going to show you how to properly handle bidirectionality in an elegant way. The technique we'll use is the replacement of lists and functions with a data structure called a telescope. This post will use Haskell exclusively, because of the limitations of JavaScript in presenting these things elegantly. I…

# Bidirectional proof refinement

16 March 2017 18 mins read

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…

In this blog post, I'm going to discuss the overall structure of a proof refinement system. Such systems can be used for implementing automatic theorem provers, proof assistants, and type checkers for programming languages. The proof refinement literature is either old or hard to understand, so this post, and subsequent ones on the same topic, will present it in a more casual…

#### Recent posts

Everything you always wanted to know about impermanent loss and were afraid to ask by Fernando Sanchez

**27 May 2022**Learn how to create low-code, low-cost financial smart contracts in the Marlowe Pioneers Program by Niamh Ahern

**11 May 2022**Project Catalyst - A virtuous cycle of Cardano ecosystem development by Tim Richmond

**10 May 2022**