Abstract
Multi-stage programming provides a new paradigm for constructing efficient solutions to complex problems. Techniques such as program generation, multi-level partial evaluation, and run-time code generation respond to the need for general purpose solutions which do not pay run-time interpretive overheads. This paper provides a foundation for the formal analysis of one such system.
We introduce a multi-stage language and present its axiomatic and reduction semantics. Our axiomatic semantics is an extension of the call-by-value λ-calculus with staging constructs. We show that staged-languages can “go Wrong” in new ways, and devise a type system that screens out such programs. Finally, we present a proof of the soundness of this type system with respect to the reduction semantics.
The research reported in this paper was supported by the USAF Air Materiel Command, contract # F19628-93-C-0069, and NSF Grant IRI-9625462.
Preview
Unable to display preview. Download preview PDF.
References
Henk P. Barendregt. The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. North-Holland, Amsterdam, 1984. Second edition.
Rowan Davies. A temporal-logic approach to binding-time analysis. In Proceedings, 11 th Annual IEEE Symposium on Logic in Computer Science, pages 184–195, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.
Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In 23rd Annual ACM Symposium on Principles of Programming Languages (POPL'96), St.Petersburg Beach, Florida, January 1996.
Robert Glück and Jesper JØrgensen. An automatic program generator for multi-level specialization. Lisp and Symbolic Computation, 10(2):113–158, 1997.
John Launchbury and Simon L. Peyton-Jones. State in haskell. Lisp and Symbolic Computation, 8(4):293–342, December 1995.
Eugenio Moggi. A categorical account of two-level languages. In MFPS 1997, 1997.
Flemming Nielson. A formal type system for comparing partial evaluators. In D BjØrner, Ershov, and Jones, editors, Proceedings of the workshop on Partial Evaluation and Mixed Computation (1987), pages 349–384. North-Holland, 1988.
Flemming Nielson. The typed λ-calculus with first-class processes. In K. Odijk, M. Rem, and J.-C. Syre, editors, PARLE '89: Parallel Languages and Architectures Europe, volume 1, pages 357–373. Springer-Verlag, New York, NY, 1989. Lecture Notes in Computer Science 365.
Flemming Nielson and Hanne Rijs Nielson. Two-Level Functional Languages. Number 34 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.
Gordon D Plotkin. A Structural Approach to Operational Semantics. Tech. Rep. FN-19, DAIMI, Univ. of Aarhus, Denmark, September 1981.
Calton Pu, Andrew Black, Crispin Cowan, and Jonathan Walpole. Microlanguages for operating system specialization. In Proceedings of the SIGPLAN Workshop on Domain-Specific Languages, Paris, January 1997.
Walid Taha and Jim Hook. The anatomy of a component generation system. In International Workshop on the Principles of Software Evolution, Kyoto, Japan, April 1998.
Walid Taha and Tim Sheard. Multi-stage programming with explicit annotations.In Proceedings of the ACM-SIGPLAN Symposium on Partial Evaluation and semantic based program manipulations PEPM'97, Amsterdam, pages 203–217. ACM, 1997.
Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 15 November 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Taha, W., Benaissa, ZEA., Sheard, T. (1998). Multi-stage programming: axiomatization and type safety. In: Larsen, K.G., Skyum, S., Winskel, G. (eds) Automata, Languages and Programming. ICALP 1998. Lecture Notes in Computer Science, vol 1443. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055113
Download citation
DOI: https://doi.org/10.1007/BFb0055113
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64781-2
Online ISBN: 978-3-540-68681-1
eBook Packages: Springer Book Archive