Sciweavers

Share
CADE
2006
Springer

Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach

12 years 5 months ago
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach
In this paper, we discuss a lightweight approach to eliminate the overhead due to implicit type arguments during higher-order unification of dependently-typed terms. First, we show that some implicit type information is uniquely determined, and can therefore be safely skipped during higher-order unification. Second, we discuss its impact in practice during type reconstruction and during proof search within the logical framework Twelf. Our experimental results show that implicit type arguments are numerous and large in size, but their impact on run-time is between 10% and 20%. On the other hand optimizations such as eliminating the occurs check are shown to be crucial to achieve significant performance improvements.
Brigitte Pientka
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Brigitte Pientka
Comments (0)
books