Higher-order uncurrying

John Joseph Hannan, Patrick Hicks

Research output: Contribution to journalArticle

4 Citations (Scopus)

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

Original languageEnglish (US)
Pages (from-to)179-216
Number of pages38
JournalHigher-Order and Symbolic Computation
Volume13
Issue number3
DOIs
StatePublished - Sep 1 2000

Fingerprint

Specifications
Polymorphism
Semantics
Acoustic waves
Formal specification

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications

Cite this

Hannan, John Joseph ; Hicks, Patrick. / Higher-order uncurrying. In: Higher-Order and Symbolic Computation. 2000 ; Vol. 13, No. 3. pp. 179-216.
@article{0c5af6edeba54e4e82c7d088e51ea610,
title = "Higher-order uncurrying",
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 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 typeable 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 richer form of unCurrying than is currently found in compilers for functional languages.",
author = "Hannan, {John Joseph} and Patrick Hicks",
year = "2000",
month = "9",
day = "1",
doi = "10.1023/A:1010006229549",
language = "English (US)",
volume = "13",
pages = "179--216",
journal = "LISP and Symbolic Computation",
issn = "1388-3690",
publisher = "Springer Netherlands",
number = "3",

}

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

In: Higher-Order and Symbolic Computation, Vol. 13, No. 3, 01.09.2000, p. 179-216.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Higher-order uncurrying

AU - Hannan, John Joseph

AU - Hicks, Patrick

PY - 2000/9/1

Y1 - 2000/9/1

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

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

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

U2 - 10.1023/A:1010006229549

DO - 10.1023/A:1010006229549

M3 - Article

AN - SCOPUS:0034268990

VL - 13

SP - 179

EP - 216

JO - LISP and Symbolic Computation

JF - LISP and Symbolic Computation

SN - 1388-3690

IS - 3

ER -