Sciweavers

TPHOL
2007
IEEE
13 years 10 months 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...
Brigitte Pientka