[isabelle] New AFP Entry: Formally Proving a Compiler Transformation Safe

Joachim Breitne has contributed a very substantial entry, entitled â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.

Preprint online here:

Once again, itâs really great to see such impressive work!

Larry Paulson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.