Blog > Authors > Rebecca Valentine

Telescopic Proof Refinement

2 January 2018 Rebecca Valentine 12 mins read

Telescopic Proof Refinement - Input Output

Telescopic Proof Refinement

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 Rebecca Valentine 18 mins read

Bidirectional proof refinement - Input Output

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…

Proof refinement basics

7 March 2017 Rebecca Valentine 19 mins read

Proof Refinement Basics - Input Output

Proof refinement basics

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…