From higher-order functional to nullary intensional

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.