Environment Classifiers
2003 (English)In: POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, New York, NY: ACM Press, 2003, Vol. 38, p. 26-37Conference paper, Published paper (Refereed)
Abstract [en]
This paper proposes and develops the basic theory for a new approach to typing multi-stage languages based a notion of environment classifiers. This approach involves explicit but lightweight tracking - at type-checking time - of the origination environment for future-stage computations. Classification is less restrictive than the previously proposed notions of closedness, and allows for both a more expressive typing of the "run" construct and for a unifying account of typed multi-stage programming. The proposed approach to typing requires making cross-stage persistence (CSP) explicit in the language. At the same time, it offers concrete new insights into the notion of levels and in turn into CSP itself. Type safety is established in the simply-typed setting. As a first step toward introducing classifiers to the Hindley-Milner setting, we propose an approach to integrating the two, and prove type preservation in this setting.
Place, publisher, year, edition, pages
New York, NY: ACM Press, 2003. Vol. 38, p. 26-37
Series
ACM / SIGPLAN Notices, ISSN 0362-1340 ; 1
Keywords [en]
Multi-stage programming, type systems, type safety, linear temporal logic, modal logic
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:hh:diva-20980DOI: 10.1145/640128.604134ISI: 000181435700004Scopus ID: 2-s2.0-1442265570Libris ID: 12438664ISBN: 1-58113-628-5 OAI: oai:DiVA.org:hh-20980DiVA, id: diva2:588279
Conference
POPL'03 – International Conference on Principles of Programming Languages, New Orleans, Louisiana, USA, January 15–17, 2003
Note
W. T. supported by NSF ITR-0113569. This work was done at Yale University.
2013-01-152013-01-142021-05-11Bibliographically approved