### Abstract

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 which 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 which 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, which implements the 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 richer form of unCurrying than is currently found in compilers for functional languages.

Original language | English (US) |
---|---|

Pages (from-to) | 1-10 |

Number of pages | 10 |

Journal | Conference Record of the Annual ACM Symposium on Principles of Programming Languages |

State | Published - 1998 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Software

### Cite this

*Conference Record of the Annual ACM Symposium on Principles of Programming Languages*, 1-10.

}

*Conference Record of the Annual ACM Symposium on Principles of Programming Languages*, pp. 1-10.

**Higher-order unCurrying.** / Hannan, John Joseph; Hicks, Patrick.

Research output: Contribution to journal › Article

TY - JOUR

T1 - Higher-order unCurrying

AU - Hannan, John Joseph

AU - Hicks, Patrick

PY - 1998

Y1 - 1998

N2 - 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 which 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 which 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, which implements the 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 richer form of unCurrying than is currently found in compilers for functional languages.

AB - 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 which 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 which 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, which implements the 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 richer form of unCurrying than is currently found in compilers for functional languages.

UR - http://www.scopus.com/inward/record.url?scp=0031679328&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031679328&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0031679328

SP - 1

EP - 10

JO - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

JF - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

SN - 0730-8566

ER -