Title: From higher-order functional to nullary intensional.
Abstract:
The aim of this paper is the mechanical proof of correctness
of the transformation proposed by P. Rondogiannis and W.~W.~Wadge,
in which a broad class of higher-order functional programs can be transformed
into semantically equivalent multidimensional intensional programs that contain
only nullary variable definitions.
The proposed algorithm systematically eliminates user-defined
functions from the source program, by appropriately introducing context
manipulation (i.e. intensional) operators. The transformation takes place
in M steps, where M is the order of the initial functional program.
During each step the order of the program is reduced by one, and the final
outcome of the algorithm is an $M$-dimensional intensional program of order
zero.As the resulting intensional code can be executed in a purely tagged-dataflow
way, the proposed approach offers a promising new technique for the
implementation of higher-order functional languages. The proof was written in Coq.