More Web Proxy on the site http://driver.im/

Article

Free access

Typed closure conversion

Authors:

Yasuhiko Minamide,

Greg Morrisett,

Robert HarperAuthors Info & Claims

POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 271 - 283

https://doi.org/10.1145/237721.237791

Published: 01 January 1996 Publication History

Abstract

Closure 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.

References

[1]

A. W. Appel. Compiling with Contmuations. Cambridge University Press, 1992.

Digital Library

[2]

A. W. Appel and T. Jim. Continuation-passing, closurepassing style. In A CM Syrup. on Prme#ples of Programmzng Languages, 1989.

Digital Library

[3]

D. E. Britton. Heap storage management for the programming language Pascal. Master's thews, Universlty of Arizona, 1975.

[4]

L. Cardelli. The functional abstract machine. Polymorph#sm, i(i), 1983.

[5]

C Cousineau, P-L Curien, and M. Mauny. The categorical abstract machine. In Functional Programming Lanquages and Computer Architecture, pages 50-64, 1985.

Digital Library

[6]

tt Friedman. Equahty between functionals. In R. Parikh, editor, Logic Colloquzum '75 Norh-Holland, 1975.

[7]

J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts #n Theoretical Computer Sczence. Cambridge University Press, Cambridge, England, 1989.

Digital Library

[8]

J. Gosling. Java mtermediate bytecodes. In A CM StG- PLAN Workshop on Intermediate Representations (IR'95), Jan. 1995

Digital Library

[9]

J. Hannan. A type system for closure conversion. In The Workshop on Types for Proqram Analyszs, 1995.

[10]

R. Harper and M. Lillibridge. Exphcit polymorphmm and CPS conversion. In ACM Syrup. on Princzples of Programmmg Languages, 1993.

Digital Library

[11]

R. Harper and M. Lillibridge A type-theoretic approach to higher-order modules. In A CM Syrup. on Prznc#ples of Programming Languages, pages 123-137, 1994.

Digital Library

[12]

R. Harper, D. MacQueen, and R. Milner Standard ML Technical Report ECS-LFCS-86-2, Laboratory for the Foundations of Computer Science# Edinburgh University. Mar. 1986

[13]

t#. Harper and J. C. Mitchell. On the type structure of 3tandard ML A CM Transaction on Programm#n9 Languages and Systems, 15(2), 1993

Digital Library

[14]

R Harper and G. Morrisett. Complhng potymorphism using intensional type analysis In A CM Syrup. on Prmc#ples of Programmmg Languages, pages 130-141, 1995.

Digital Library

[15]

T. Johnsson. Lambda lifting- Transformmg programs to recursive equations. In Functional Programming Language and Computer Architecture, LNCS 201, pages 190-203. Springer- Verlag, 1985.

Digital Library

[16]

R. Kelsey and P. Hudak. Realistic compilation by program translation -detailed summary-. In A CM Syrup. on Pmnc#ples of Programming Languages, pages 281-292, 1989.

Digital Library

[17]

D. Kranz et al. Orbit: An optimizing compiler for Scheme. In Proc. of the SIGPLAN '86 Syrup. on Compiler Constructzon, 1986.

Digital Library

[18]

X. Leroy. Unboxed objects and polymorphic typing. In A CM Symp. on Principles o/Programming Languages, 1992.

Digital Library

[19]

X. Leroy. Manifest types, modules, and separate compilation. In A CM Symp. on Pmnczples of Programming Languages, pages 109-122, 1994.

Digital Library

[20]

D. MacQueen. Modules for Standard ML. In Proc. ACM Conf. Lisp and Functional Programmzng, pages 198-207, 1984. Revised version appears in {12}.

Digital Library

[21]

Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. Technical Report CMU-CS-95-171, School of Computer Science, Carnegie Mellon University, July 1995.

[22]

J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. A CM Transactwn on Programming Languages and Systems, 10(3), 1988.

Digital Library

[23]

G. Morrisett, M. FeIIeisen, and R. Harper. Abstract models of memory management. In Functwnal Programm,ng Languages and Computer Architecture, pages 66-77, June 1995.

Digital Library

[24]

R. Morrison, A. Dearle, R. Connor, and A. L. Brown. An ad hoc approach to the implementation of polymorphism. A CM Transactwn on Programming Languages and Systems, 13(3), 1991.

Digital Library

[25]

A. Ohori. A compilation method for ML-style polymorphic record calculi. In A CM Symp. on Principles of Programming Languages, 1992.

Digital Library

[26]

B. C Pierce and D. N. T#rner. Simple type-theoretic foundations for object-oriented programming. Journal of Functzonal Programming, 4(2):207-247, Apr. 1994. A preliminary version appeared in Principles of Programming Languages, 1993, and as University of Edinburgh technical report ECS- LFCS-92-225, under the title "Object-Oriented Programming Without Recursive Types".

[27]

G. D. Plotkin. Lambda-definability in the full type hierarchy. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.

[28]

U. S. Reddy. Objects as closures. In Proe. ACM Conf. Lisp and Functional Programming, 1988.

[29]

J. C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the Annual A CM Conference, pages 717-740, 1972.

Digital Library

[30]

Z. Shao and A. W. Appel. Space-efficient closure representations. In Proc. A CM Conf. Lzsp and Functional Programming, 1994.

Digital Library

[31]

Z. Shao and A. W. Appel. A type-based compiler for Standard ML. In Programming Language Design and Its zmplemenation, pages 116-129, 1995.

Digital Library

[32]

R. Statman. Completeness, invariance, and lambdadefinability. Journal of Symbolic Logic, 47:17-26, 1982.

[33]

R. Statman. Logical relations and the typed A-calculus. informatzon and Control, 65, 1985.

[34]

G. L. Steele Jr. Rabbit: A compiler for Scheme. Master's thesis, MIT, 1978.

[35]

W.W. Tait. Intensionat interpretation of functionals of finite type. Journal of Symbohc Logic, 32(2), 1967.

[36]

D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. Technical report, School of Computer Science, Carnegie Mellon University, Oct. 1995. To appear.

[37]

A. Tolmach. Tag-free garbage collection using explicit type parameters. In Proc. A CM Conf. Lisp and Functional Programmmg, pages 1-11, June 1994.

Digital Library

[38]

R. Wahbe, S. Lucco, T. Anderson, and S. Graham. Efficient software-based fault isolation. In 14th ACM Symposium on Operating Systems Pmnczples, Dec. 1993.

Digital Library

[39]

M. Wand and P. Steckler. Selective and lightweight closure conversion. In A CM Symp. on Principles of Programming Languages, 1994.

Digital Library

Cited By

Downen P(2024)Call-by-Unboxed-ValueProceedings of the ACM on Programming Languages10.1145/36746548:ICFP(845-879)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674654
Fitzgibbons MParaskevopoulou ZMushtak NThalakottur MSulaiman Manzur JAhmed A(2024)RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssemblyProceedings of the ACM on Programming Languages10.1145/36564448:PLDI(1656-1679)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656444
Smeding TVákár M(2024)Efficient CHADProceedings of the ACM on Programming Languages10.1145/36328788:POPL(1060-1088)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632878
Show More Cited By

Index Terms

Typed closure conversion
1. Software and its engineering
  1. Software notations and tools
    1. Compilers

Recommendations

Typed closure conversion for the calculus of constructions
PLDI '18

Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the ...
Typed closure conversion for the calculus of constructions
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation

Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the ...
Typed Closure Conversion for Recursively-Defined Functions

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1996

423 pages

ISBN:0897917693

DOI:10.1145/237721

Chairman:
Hans-J. Boehm
Xerox Palo Alto Research Center,Palo Alto,CA
,
Conference Chair:
Guy Steele
Sun Microsystems Labs.

Copyright © 1996 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1996

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL96

Sponsor:

POPL96: 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 21 - 24, 1996

Florida, St. Petersburg Beach, USA

Acceptance Rates

POPL '96 Paper Acceptance Rate 34 of 148 submissions, 23%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

148
Total Citations
View Citations
471
Total Downloads

Downloads (Last 12 months)156
Downloads (Last 6 weeks)18

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Downen P(2024)Call-by-Unboxed-ValueProceedings of the ACM on Programming Languages10.1145/36746548:ICFP(845-879)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674654
Fitzgibbons MParaskevopoulou ZMushtak NThalakottur MSulaiman Manzur JAhmed A(2024)RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssemblyProceedings of the ACM on Programming Languages10.1145/36564448:PLDI(1656-1679)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656444
Smeding TVákár M(2024)Efficient CHADProceedings of the ACM on Programming Languages10.1145/36328788:POPL(1060-1088)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632878
Brandon WDriscoll BDai FBerkow WMilano M(2023)Better Defunctionalization through Lambda Set SpecializationProceedings of the ACM on Programming Languages10.1145/35912607:PLDI(977-1000)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591260
Huang YYallop J(2023)Defunctionalization with Dependent TypesProceedings of the ACM on Programming Languages10.1145/35912417:PLDI(516-538)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591241
Leijen DLorenzen A(2023)Tail Recursion Modulo Context: An Equational ApproachProceedings of the ACM on Programming Languages10.1145/35712337:POPL(1152-1181)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571233
Odersky MBoruch-Gruszecki ABrachthäuser JLee ELhoták ORichard-Foy JDoeraene S(2021)Safer exceptions for ScalaProceedings of the 12th ACM SIGPLAN International Symposium on Scala10.1145/3486610.3486893(1-11)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1145/3486610.3486893
Merigoux DChataing NProtzenko J(2021)Catala: a programming language for the lawProceedings of the ACM on Programming Languages10.1145/34735825:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473582
Sullivan ZDownen PAriola ZLindley SMogensen T(2021)Strictly capturing non-strict closuresProceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3441296.3441398(74-89)Online publication date: 18-Jan-2021
https://dl.acm.org/doi/10.1145/3441296.3441398
Ricciotti WCheney J(2021)Query LiftingProgramming Languages and Systems10.1007/978-3-030-72019-3_21(579-606)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_21
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents