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.
CITATION STYLE
Pientka, B., & Pfenning, F. (2003). Optimizing higher-order pattern unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2741, pp. 473–487). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_40
Mendeley helps you to discover research relevant for your work.