ブログ > 筆者 > Rebecca Valentine

Telescopic Proof Refinement

2018年 1月 2日 Rebecca Valentine 12 分で読めます

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

2017年 3月 16日 Rebecca Valentine 18 分で読めます

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

2017年 3月 7日 Rebecca Valentine 19 分で読めます

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…

Telescopic Proof Refinement

2018年 1月 2日 Rebecca Valentine 12 分で読めます

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

2017年 3月 16日 Rebecca Valentine 18 分で読めます

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…

1

2