Optimizing Higher-Order Pattern Unification

11 years 6 months ago
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.
Brigitte Pientka, Frank Pfenning
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where CADE
Authors Brigitte Pientka, Frank Pfenning
Comments (0)