Abstract
Safely adding computational effects to a multi-stage language has been an open problem. In previous work, a closed type constructor was used to provide a safe mechanism for executing dynamically generated code. This paper proposes a general notion of closed type as a simple approach to safely introducing computational effects into multi-stage languages. We demonstrate this approach formally in a core language called Mini-MLref BN. This core language combines safely multi-stage constructs and ML-style references. In addition to incorporating state, Mini-ML ref BN also embodies a number of technical improvements over previously proposed core languages for multi-stage programming.
Research partially supported by MURST and ESPRIT WG APPSEM.
Postdoctoral Fellow funded by the Swedish Research Council for Engineering Sciences (TFR), grant number 221-96-403.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Zine El-Abidine Benaissa, Eugenio Moggi, Walid Taha, and Tim Sheard. Logical modalities and multi-stage programming. In Federated Logic Conference (FLoC) Satellite Workshop on Intuitionistic Modal Logics and Applications (IMLA), July 1999.
Dominique Clement, Joelle Despeyroux, Thierry Despeyroux, and Gilles Kahn. A simple applicative language: Mini-ML. In Proceedings of the 1986 ACM Conference on Lisp and Functional Programming, pages 13–27. ACM, ACM, August 1986.
Rowan Davies. A temporal-logic approach to binding-time analysis. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 184–195, New Brunswick, 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), pages 258–270, St. Petersburg Beach, January 1996.
Carsten K. Gomard and Neil D. Jones. A partial evaluator for untyped lambda calculus. Journal of Functional Programming, 1(1):21–69, January1991.
Robert Glück and Jesper Jorgensen. Fast binding-time analysis for multi-level specialization. In Dines Bjorner, Manfred Broy, and Igor V. Pottosin, editors, Perspectives of System Informatics, volume 1181 of Lecture Notes in Computer Science, pages 261–272. Springer-Verlag, 1996.
John Hatcliff and Olivier Danvy. A computational formalization for partial evaluation. Mathematical Structures in Computer Science, 7(5):507–541, October 1997.
Neil D. Jones, Carsten K Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.
The MetaML Home Page, 2000. Provides source code and documentation online at http://www.cse.ogi.edu/PacSoft/projects/metaml/index.html.
Eugenio Moggi. Functor categories and two-level languages. In FoSSaCS’ 98, volume 1378 of Lecture Notes in Computer Science. Springer Verlag, 1998.
Eugenio Moggi, Walid Taha, Zine El-Abidine Benaissa, and Tim Sheard. An idealized MetaML: Simpler, and more expressive. In European Symposium on Programming (ESOP), volume 1576 of Lecture Notes in Computer Science, pages 193–207. Springer-Verlag, 1999.
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1:125–159, 1975.
Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, July 1999.
Walid Taha. A sound reduction semantics for untyped CBN multi-stage computation. Or, the theory of MetaML is non-trivial. In Proceedings of the ACM Symposium on Partial Evaluation and Semantics Based Program Manipulation, Boston, January2000.
Walid Taha, Zine-El-Abidine Benaissa, and Tim Sheard. Multi-stage programming: Axiomatization and type-safety. In 25th International Colloquium on Automata, Languages, and Programming, volume 1443 of Lecture Notes in Computer Science, pages 918–929, Aalborg, July 1998.
Peter Thiemann and Dirk Dussart. Partial evaluation for higher-order languages with state. Available online from http://www.informatik.unifreiburg.de/~thiemann/papers/index.html.
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.
Walid Taha and Tim Sheard. MetaML: Multi-stage programming with explicit annotations. Theoretical Computer Science, 248(1–2), 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Calcagno, C., Moggi, E., Taha, W. (2000). Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds) Automata, Languages and Programming. ICALP 2000. Lecture Notes in Computer Science, vol 1853. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45022-X_4
Download citation
DOI: https://doi.org/10.1007/3-540-45022-X_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67715-4
Online ISBN: 978-3-540-45022-1
eBook Packages: Springer Book Archive