Typed Closure Conversion
Yasuhiko Minamide, Greg Morrisett, and Robert Harper


We study the typing properties of closure conversion for simply-typed
and polymorphic lambda-calculi.  Unlike most accounts of closure
conversion, which only treat the untyped lambda-calculus, we translate
well-typed source programs to well-typed target programs.  This allows
later compiler phases to take advantage of types for representation
analysis and tag-free garbage collection, and it facilitates
correctness proofs.  Our account of closure conversion for the
simply-typed language takes advantage of a simple model of objects by
mapping closures to existentials.  Closure conversion for the
polymorphic language requires additional type machinery, namely
translucency in the style of Harper and Lillibridge's module calculus,
to express the type of a closure.