Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Much recent work on the compilation of statically typed languages such as ML relies on the propagation of type information from source to object code in order to increase the reliability and maintainabilty of the compiler itself and to improve the efficiency and verifiability of generated code. To achieve this the program transformations performed by a compiler must be cast as type-preserving translations between typed intermediate languages. In earlier work with Minamide we studied one important compiler transformation, closure conversion, for the case of pure simply-typed and polymorphic $\lambda$-calculus. Here we extend the treatment of simply-typed closure conversion to account for recursively-defined functions such as are found in ML. We consider three main approaches, one based on a recursive code construct, one based on a self-referential data structure, and one based on recursive types. We discuss their relative advantages and disadvantages, and sketch correctness proofs for these transformations based on the method of logical relations.