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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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)
Barendregt, H.: The Lambda Calculus — Its Syntax and Semantics. North-Holland (1984)
Bawden, A.: Quasiquotation in Lisp. In: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, San Antonio, Texas (1999)
Benaissa, Z.-E.-A., Moggi, E., Taha, W., Sheard, T.: Logical modalities and multi-stage programming. In: Proceedings of the Workshop on Intuitionistic Modal Logics and Applications, Trento, Italy (July 1999)
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)
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)
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)
Chen, C., Xi, H.: Meta-programming through typeful code representation. Journal of Functional Programming 15(6), 797–835 (2005)
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)
Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of the ACM 48(3), 555–604 (2001)
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)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. International Series in Computer Science. Prentice-Hall (1993)
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)
Kim, I.-S., Yi, K., Calcagno, C.: A polymorphic modal type system for lisp-like multi-staged languages. In: Proceedings of the Thirty-Third Annual ACM Symposium on Principles of Programming Languages, pp. 257–268. ACM Press, Charleston (2006)
McCarthy, J.: LISP 1.5 Programmer’s Manual. The MIT Press, Cambridge (1962)
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)
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)
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)
Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic 9(3), 1–49 (2008)
Pierce, B.C.: Types and Programming Languages. The MIT Press, Cambridge (2002)
Rhiger, M.: First-class open and closed code fragments. Trends in Functional Programming 6, 127–144 (2007), Intellect
Taha, W.: Multi-Stage programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology (1999)
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)
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)
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)
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)
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)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115, 38–94 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rhiger, M. (2012). Staged Computation with Staged Lexical Scope. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)