48: Reflective Proof Theory

Beginning with a set of interactive rewrite rules, Greg Meredith discusses his work with Mike Stay to derive a proof theory that exhibits a Curry-Howard style correspondence. Specifically, it enjoys a cut-elimination property that mirrors the notion of compute in the rewrite rules. Isaac DeFrain and Christian Williams join the conversation. Visit the blog for the corresponding slides.

Leave a Reply

Your email address will not be published. Required fields are marked *