Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
In this proof pearl, the authors demonstrate the power of higher-order encodings in the logical framework Twelf[PS99] by investigating proofs about an algorithmic specification of bounded subtype polymorphism, a problem from the POPLmark challenge [ABF+05]. Their encoding and representation of the problem plays to the strengths of the logical framework LF. Higher-order abstract syntax is used to deal with issues of bound variables. More importantly, they exploit the full advantage of parametric and higher-order judgments. As a key benefit they get a tedious narrowing lemma, which must normally be proven separately, for free. Consequently, they obtain an extremely compact and elegant encoding of the admissibility of general transitivity and other meta-theoretic properties.