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.