Journal Article: The Safety of Call Arity

We formalize the Call Arity analysis, as implemented in GHC, and prove both functional correctness and, more interestingly, safety (i.e. the transformation does not increase allocation). We use Christian Urban's Nominal2 package to define our terms. The functional correctness is defined with regard to a standard denotational semantics. The operational properties are shown with regard to a small-step semantics akin to Sestoft's mark 1 machine. We make use of Brian Huffman's HOLCF package for the domain-theoretical aspects of the development.