Abstract
We develop yet another typed multi-stage calculus λ ⊳ %. It extends Tsukada and Igarashi’s λ ⊳ with cross-stage persistence and is equipped with all the key features that MetaOCaml-style multi-stage programming supports. It has an arguably simple, substitution-based full-reduction semantics and enjoys basic properties of subject reduction, confluence, and strong normalization. Progress also holds under an alternative semantics that takes staging into account and models program execution. The type system of λ ⊳ % gives a sufficient condition when residual programs can be safely generated, making λ ⊳ % more suitable for writing generating extensions than previous multi-stage calculi.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
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
Taha, W.: A gentle introduction to multi-stage programming. In: Lengauer, C., Batory, D., Blum, A., Odersky, M. (eds.) Domain-Specific Program Generation. LNCS, vol. 3016, pp. 30–50. Springer, Heidelberg (2004)
Sheard, T., Peyton Jones, S.: Template meta-programming for Haskell. In: Proceedings of Haskell Workshop (Haskell 2002), pp. 60–75 (2002)
Taha, W., Sheard, T.: MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science 248, 211–242 (2000)
Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementing multi-stage languages using ASTs, gensym, and reflection. In: Pfenning, F., Macko, M. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 57–76. Springer, Heidelberg (2003)
Kim, I.S., Yi, K., Calcagno, C.: A polymorphic modal type system for Lisp-like multi-staged languages. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006), Charleston, SC, pp. 257–268 (January 2006)
Chen, C., Xi, H.: Meta-programming through typeful code representation. In: Proceedings of ACM International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden, pp. 275–286 (August 2003)
Mainland, G.: Explicitly heterogeneous metaprogramming with MetaHaskell. In: Proceedings of ACM International Conference on Functional Programming (ICFP 2012), Copenhagen, Denmark, pp. 311–322 (September 2012)
Taha, W., Nielsen, M.F.: Environment classifiers. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2003), pp. 26–37 (2003)
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)
Tsukada, T., Igarashi, A.: A logical foundation for environment classifiers. Logical Methods in Computer Science 6(4:8), 1–43 (2010)
Benaissa, Z.E.A., Moggi, E., Taha, W., Sheard, T.: Logical modalities and multi-stage programming. In: Proceedings of Workshop on Intuitionstic Modal Logics and Applications (IMLA 1999) (1999)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall (1993)
Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120–127 (1995)
Davies, R.: A temporal-logic approach to binding-time analysis. In: Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 184–195. IEEE Computer Society Press (July 1996)
Glück, R., Jørgensen, J.: Efficient multi-level generating extensions for program specialization. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol. 982, pp. 259–278. Springer, Heidelberg (1995)
Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of the ACM 48(3), 555–604 (2001)
Yuse, Y., Igarashi, A.: A modal type system for multi-level generating extensions with persistent code. In: Proceedings of the 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2006), Venice, Italy, pp. 201–212 (2006)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Hanada, Y., Igarashi, A. (2014). On Cross-Stage Persistence in Multi-Stage Programming. In: Codish, M., Sumii, E. (eds) Functional and Logic Programming. FLOPS 2014. Lecture Notes in Computer Science, vol 8475. Springer, Cham. https://doi.org/10.1007/978-3-319-07151-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-07151-0_7
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07150-3
Online ISBN: 978-3-319-07151-0
eBook Packages: Computer ScienceComputer Science (R0)