A logical framework is a general meta-language for specifying and implementing deductive systems, given by axioms and inference rules. Based on a higher-order logic programming interpretation, it supports executing logical systems and reasoning with and about them, thereby reducing the effort required for each particular logical system.

In this thesis, we describe different techniques to improve the overall performance and the expressive power of higher-order logic programming. First, we introduce tabled higher-order logic programming, a novel execution model where some redundant information is eliminated using selective memoization. This extends tabled computation to the higher-order setting and forms the basis of the tabled higher-order logic programming interpreter. Second, we present efficient data-structures and algorithms for higher-order proof search. In particular, we describe a higher-order assignment algorithm which eliminates many unnecessary occurs checks and develop higher-order term indexing. These optimizations are crucial to make tabled higher-order logic programming successful in practice. Finally, we use tabled proof search in the meta-theorem prover to reason efficiently with and about deductive systems. It takes full advantage of higher-order assignment and higher-order term indexing.

As experimental results demonstrate, these optimizations taken together constitute a significant step toward exploring the full potential of logical frameworks in practice.

235 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu