Higher-Order Abstract Syntax in Coq
TLCA, pp. 124-138, 1995.
higher-order abstract syntaxsecond ordertyped lambda calculusprogramming languagenatural deduction
The terms of the simply-typed lambda-calculus can be used to express the higher-order abstract syntax of objects such as logical formulas, proofs, and programs. Support for the manipulation of such objects is provided in several programming languages (e.g. lambdaProlog, Elf). Such languages also provide embedded implication, a tool which...更多