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...
The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this meth...
Dependently typed -calculi such as the Logical Framework (LF) are capable of representing relationships between terms through types. By exploiting the "formulas-as-types"...