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

Article

Staged computation with staged lexical scope

Author:

Morten RhigerAuthors Info & Claims

ESOP'12: Proceedings of the 21st European conference on Programming Languages and Systems

Pages 559 - 578

https://doi.org/10.1007/978-3-642-28869-2_28

Published: 24 March 2012 Publication History

Abstract

We present a simple core type system, λ^{[ ]} -- pronounced "lambda open box" -- for a statically typed, hygienic, and multi-stage lambda-calculus supporting evaluation under future-stage binders, open-code manipulation, a first-class eval function, and mutable state. The type system provides one type of lexically scoped code that precisely accounts for the contexts in which code values can be inserted. In particular, this type can distinguish between open and closed code. We show how to extend λ^{[ ]} with subtype polymorphism over program contexts. The soundness and simplicity of λ^{[ ]} demonstrate that the notion of staging is orthogonal to features that have been presented as instrumental in existing type systems for staged computation, such as polymorphism, nameless term representations, explicit substitutions, and delimited continuations.

References

[1]

Backus, J. W., Beeber, R. J., Best, S., Goldberg, R., Haibt, L. M., Herrick, H. L., Nelson, R. A., Sayre, D., Sheridan, P. B., Stern, H., Ziller, I., Hughes, R. A., Nutt, R.: The Fortran automatic coding system. In: Techniques for Reliability, Proceedings of the Western Joint Computer Conference, pp. 188-198 (1957)

Digital Library

[2]

Barendregt, H.: The Lambda Calculus -- Its Syntax and Semantics. North-Holland (1984)

[3]

Bawden, A.: Quasiquotation in Lisp. In: Proceedings of the ACMSIGPLANWorkshop on Partial Evaluation and Semantics-Based Program Manipulation, San Antonio, Texas (1999)

[4]

Benaissa, Z.-E.-A., Moggi, E., Taha, W., Sheard, T.: Logical modalities and multistage programming. In: Proceedings of the Workshop on Intuitionistic Modal Logics and Applications, Trento, Italy (July 1999)

[5]

Bondorf, A., Jones, N. D., Mogensen, T., Sestoft, P.: Binding time analysis and the taming of self-application. DIKU rapport, University of Copenhagen, Copenhagen, Denmark (1988)

[6]

Calcagno, C., Moggi, E., Taha, W.: Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming. In: Welzl, E., Montanari, U., Rolim, J. D. P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 25-36. Springer, Heidelberg (2000)

Digital Library

[7]

Calcagno, C., Moggi, E., Taha, W.: ML-Like Inference for Classifiers. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 79-93. Springer, Heidelberg (2004)

[8]

Chen, C., Xi, H.: Meta-programming through typeful code representation. Journal of Functional Programming 15(6), 797-835 (2005)

Digital Library

[9]

Davies, R.: A temporal-logic approach to binding-time analysis. In: Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pp. 184-195. IEEE Computer Society Press, New Brunswick (1996)

Digital Library

[10]

Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of the ACM 48(3), 555-604 (2001)

Digital Library

[11]

Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Technical Report Rice COMP TR89-100, Department of Computer Science, Rice University, Houston, Texas (June 1989)

[12]

Jones, N. D., Gomard, C. K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. International Series in Computer Science. Prentice-Hall (1993)

Digital Library

[13]

Kameyama, Y., Kiselyov, O., Shan, C.C.: Shifting the stage: staging with delimited control. In: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 111-120. ACM, Savannah (2009)

Digital Library

[14]

Kim, I.-S., Yi, K., Calcagno, C.: A polymorphic modal type system for lisplike multi-staged languages. In: Proceedings of the Thirty-Third Annual ACM Symposium on Principles of Programming Languages, pp. 257-268. ACM Press, Charleston (2006)

Digital Library

[15]

McCarthy, J.: LISP 1.5 Programmer's Manual. The MIT Press, Cambridge (1962)

Digital Library

[16]

Moggi, E., Taha, W., Benaissa, Z.-E.-A., Sheard, T.: An Idealized MetaML: Simpler, and More Expressive. In: Swierstra, S. D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 193-207. Springer, Heidelberg (1999)

Digital Library

[17]

Morrisett, G., Felleisen, M., Harper, R.: Abstract models of memory management. In: Proceedings of the Seventh ACM Conference on Functional Programming and Computer Architecture, pp. 66-77. ACM Press, La Jolla (1995)

Digital Library

[18]

Nanevski, A.: Meta-programming with names and necessity. In: Proceedings of the 2002 ACM SIGPLAN International Conference on Functional Programming, pp. 206-217. ACM Press, Pittsburgh (2002)

Digital Library

[19]

Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic 9(3), 1-49 (2008)

Digital Library

[20]

Pierce, B.C.: Types and Programming Languages. The MIT Press, Cambridge (2002)

Digital Library

[21]

Rhiger, M.: First-class open and closed code fragments. Trends in Functional Programming 6, 127-144 (2007), Intellect

[22]

Taha, W.: Multi-Stage programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology (1999)

Digital Library

[23]

Taha, W.: A sound reduction semantics for untyped CBN multi-stage computations. or, the theory of MetaML is non-trivial. In: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation. ACM Press, Boston (2000)

Digital Library

[24]

Taha, W., Benaissa, Z.-E.-A., Sheard, T.: Multi-Stage Programming: Axiomatization and Type Safety. In: Larsen, K. G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 918-929. Springer, Heidelberg (1998)

Digital Library

[25]

Taha, W., Nielsen, M. F.: Environment classifiers. In: Proceedings of the Thirtieth Annual ACM Symposium on Principles of Programming Languages, pp. 26-37. ACM Press, New Orleans (2003)

Digital Library

[26]

Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 203-217. ACM Press, Amsterdam (1997)

Digital Library

[27]

Westbrook, E., Ricken, M., Inoue, J., Yao, Y., Abdelatif, T., Taha, W.: Mint: Java multi-stage programming using weak separability. In: Proceedings of the ACM SIGPLAN 2010 Conference on Programming Languages Design and Implementation, pp. 400-411. ACM Press, Toronto (2010)

Digital Library

[28]

Wright, A. K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115, 38-94 (1994)

Digital Library

Cited By

Gao CParreaux LChiba SThüm T(2024)Seamless Scope-Safe Metaprogramming through Polymorphic Subtype Inference (Short Paper)Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690733(121-127)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690733
Isoda KYokoyama AKameyama YChiba SThüm T(2024)Type-Safe Code Generation with Algebraic Effects and HandlersProceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690731(53-65)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690731
Jang JGélineau SMonnier SPientka B(2022)Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itselfProceedings of the ACM on Programming Languages10.1145/34987006:POPL(1-27)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498700
Show More Cited By

Staged computation with staged lexical scope
1. Theory of computation
  1. Semantics and reasoning

Recommendations

Tagless staged interpreters for typed languages

Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving an implementation that is both readable and efficient. In an ...
Tagless staged interpreters for typed languages
ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming

Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving an implementation that is both readable and efficient. In an ...
A polymorphic modal type system for lisp-like multi-staged languages
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

This article presents a polymorphic modal type system and its principal type inference algorithm that conservatively extend ML by all of Lisp's staging constructs (the quasi-quotation system). The combination is meaningful because ML is a practical ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ESOP'12: Proceedings of the 21st European conference on Programming Languages and Systems

March 2012

599 pages

ISBN:9783642288685

Editor:
Helmut Seidl
Technische Universität München, Boltzmannstrasse 3, Garching, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 24 March 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 10 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gao CParreaux LChiba SThüm T(2024)Seamless Scope-Safe Metaprogramming through Polymorphic Subtype Inference (Short Paper)Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690733(121-127)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690733
Isoda KYokoyama AKameyama YChiba SThüm T(2024)Type-Safe Code Generation with Algebraic Effects and HandlersProceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690731(53-65)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690731
Jang JGélineau SMonnier SPientka B(2022)Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itselfProceedings of the ACM on Programming Languages10.1145/34987006:POPL(1-27)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498700
Lilis YSavidis A(2019)A Survey of Metaprogramming LanguagesACM Computing Surveys10.1145/335458452:6(1-39)Online publication date: 16-Oct-2019
https://dl.acm.org/doi/10.1145/3354584
Kameyama YKiselyov OShan CChin WHage J(2014)Combinators for impure yet hygienic code generationProceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation10.1145/2543728.2543740(3-14)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2543728.2543740
Cheney JLindley SRadanne GWadler PChin WHage J(2014)Effective quotationProceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation10.1145/2543728.2543738(15-26)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2543728.2543738
Cheney JLindley SWadler P(2013)A practical theory of language-integrated queryACM SIGPLAN Notices10.1145/2544174.250058648:9(403-416)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2544174.2500586
Cheney JLindley SWadler PMorrisett GUustalu T(2013)A practical theory of language-integrated queryProceedings of the 18th ACM SIGPLAN international conference on Functional programming10.1145/2500365.2500586(403-416)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2500365.2500586
Rhiger MDanvy O(2012)Hygienic quasiquotation in schemeProceedings of the 2012 Annual Workshop on Scheme and Functional Programming10.1145/2661103.2661109(58-64)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2661103.2661109
Lindley SLöh AGarcia R(2012)Embedding FProceedings of the 8th ACM SIGPLAN workshop on Generic programming10.1145/2364394.2364402(45-56)Online publication date: 12-Sep-2012
https://dl.acm.org/doi/10.1145/2364394.2364402

View Options

View options

Figures

Tables

Media

View Table of Conten