Typed Closure Conversion
MetadataShow full item record
CitationMinamide, Yasuhiko, Greg Morrisett, and Robert Harper. 1996. Typed closure conversion. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg Beach, Florida, United States, January 21-24, 1996): POPL '96, 271-283. New York: ACM.
AbstractClosure conversion is a program transformation used by compilers to separate code from data. Previous accounts of closure conversion use only untyped target languages. Recent studies show that translating to typed target languages is a useful methodology for building compilers, because a compiler can use the types to implement efficient data representations, calling conventions, and tag-free garbage collection. Furthermore, type-based translations facilitate security and debugging through automatic type checking, as well as correctness arguments through the method of logical relations. We present closure conversion as a type-directed, and type preserving translation for both the simply-typed and the polymorphic λ--calculus. Our translations are based on a simple "closures as objects" principle: higher-order functions are viewed as objects consisting of a single method (the code) and a single instance variable (the environment). In the simply-typed case, the Pierce-Turner model of object typing where objects are packages of existential type suffices. In the polymorphic case, more careful tracking of type sharing is required. We exploit a variant of the Harper-Lillibridge "translucent type" formalism to characterize the types of polymorphic closures.
Citable link to this pagehttp://nrs.harvard.edu/urn-3:HUL.InstRepos:3710800
- FAS Scholarly Articles