Higher-Order unCurrying

13 years 8 months ago
Higher-Order unCurrying
We present a formal specification of unCurrying for a higher-order, functional language with ML-style let-polymorphism. This specification supports the general unCurrying of functions, even for functions that are passed as arguments or returned as values. The specification also supports partial unCurrying of any consecutive parameters of a function,rather than only unCurrying all of a function’s parameters. We present the specification as a deductive system that axiomatizes a judgment relating a source term with an unCurried form of the term. We prove that this system relates only typable terms and that it is correct with respect to an operational semantics. We define a practical algorithm, based on algorithm W, that implements unCurrying and prove this algorithm sound and complete with respect to the deductive system. This algorithm generates maximally unCurried forms of source terms. These results provide a declarative framework for reasoning about unCurrying and support a ric...
John Hannan, Patrick Hicks
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where POPL
Authors John Hannan, Patrick Hicks
Comments (0)