Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF

Abstract. In this proof pearl, we demonstrate the power of higherorder 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]. Our encoding and representation of the problem plays to the strengths of the logical k LF. Higher-order abstract syntax is used to deal with issues of bound variables. More importantly, we exploit the full advantage of parametric and higher-order judgments. As a key benefit we get a tedious narrowing lemma, which must normally be proven separately, for free. Consequently, we obtain an extremely compact and elegant encoding of the admissibility of general transitivity and other meta-theoretic properties.

• Type: Conference
• Year: 2007
• Where: TPHOL
• Authors: Brigitte Pientka
• Keywords: Artificial Intelligence, Logical Framework, Proof Pearl, Tedious Narrowing Lemma, TPHOL 2007