Sciweavers

Share
TPHOL
2007
IEEE

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

9 years 16 days ago
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.
Brigitte Pientka
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where TPHOL
Authors Brigitte Pientka
Comments (0)
books