Optimizing Higher-Order Pattern Unification

Abstract. We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such as linearization, which eliminates many unnecessary occurs-checks. The presented modal framework explains a number of features of the current implementation of higher-order unification in Twelf and provides insight into several optimizations. Experimental results demonstrate significant performance improvement in many example applications of Twelf, including those in the area of proof-carrying code.

• Type: Conference
• Year: 2003
• Where: CADE
• Authors: Brigitte Pientka, Frank Pfenning
• Keywords: Automated Reasoning, CADE 2003, Modal Type Theory, Presented Modal Framework, Significant Performance Improvement