Reasoning with Higher-Order Abstract Syntax in a Logical Framework

Raymond C. McDowell, Dale A. Miller

Logical frameworks based on intuitionistic or linear logics with higher-type quantification have been successfully used to give high-level, modular, and formal specifications of ma…