Djinn, Monotonic
Conor Thomas McBride · EPiC series in computing · 2018
Dyckhoff's algorithm for contraction-free proof search in intuitionistic propositional logic (popularized by Augustsson as the type-directed program synthesis tool, Djinn) is a simple program with a rather tricky termination proof. In this talk, I describe my efforts to reduce this program to a steady structural descent. On the way, I shall present an attempt at a compositional approach to explaining termination, via a uniform presentation of memoization.