Article

Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming

Authors:

Cristiano Calcagno,

Walid TahaAuthors Info & Claims

ICALP '00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming

Pages 25 - 36

Published: 09 July 2000 Publication History

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 multistage languages. We demonstrate this approach formally in a core language called Mini-ML_ref^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.

References

[1]

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.

[2]

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.

[3]

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.

[4]

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.

[5]

Carsten K. Gomard and Neil D. Jones. A partial evaluator for untyped lambda calculus. Journal of Functional Programming, 1(1):21-69, January 1991.

[6]

Robert Glück and Jesper Jørgensen. Fast binding-time analysis for multi-level specialization. In Dines Bjørner, 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.

[7]

John Hatcliff and Olivier Danvy. A computational formalization for partial evaluation. Mathematical Structures in Computer Science, 7(5):507-541, October 1997.

[8]

Neil D. Jones, Carsten K Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.

[9]

The MetaML Home Page, 2000. Provides source code and documentation online at http://www.cse.ogi.edu/PacSoft/projects/metaml/index.html.

[10]

Eugenio Moggi. Functor categories and two-level languages. In FoSSaCS '98, volume 1378 of Lecture Notes in Computer Science. Springer Verlag, 1998.

[11]

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.

[12]

Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

[13]

Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1:125-159, 1975.

[14]

Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, July 1999.

[15]

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, January 2000.

[16]

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.

[17]

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.

[18]

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.

[19]

Walid Taha and Tim Sheard. MetaML: Multi-stage programming with explicit annotations. Theoretical Computer Science, 248(1-2), 2000.

Cited By

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
Rhiger M(2012)Staged computation with staged lexical scopeProceedings of the 21st European conference on Programming Languages and Systems10.1007/978-3-642-28869-2_28(559-578)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28869-2_28
Westbrook EFrisby NBrauner P(2011)Hobbits for HaskellACM SIGPLAN Notices10.1145/2096148.203468146:12(35-46)Online publication date: 22-Sep-2011
https://dl.acm.org/doi/10.1145/2096148.2034681
Show More Cited By

Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming
1. Theory of computation
  1. Semantics and reasoning

Recommendations

Closed types for a safe imperative MetaML

This paper addresses the issue of safely combining computational effects and multi-stage programming. We propose a type system which exploits a notion of closed type, to check statically that an imperative multi-stage program does not cause run-time ...
Quantified types in an imperative language

We describe universal types, existential types, and type constructors in Cyclone, a strongly typed C-like language. We show how the language naturally supports first-class polymorphism and polymorphic recursion while requiring an acceptable amount of ...
Existential Types for Imperative Languages
ESOP '02: Proceedings of the 11th European Symposium on Programming Languages and Systems

We integrate existential types into a strongly typed C-like language. In particular, we show how a bad combination of existential types, mutation, and aliasing can cause a subtle violation of type safety. We explore two independent ways to strengthen ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ICALP '00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming

July 2000

933 pages

ISBN:3540677151

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 09 July 2000

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Rhiger M(2012)Staged computation with staged lexical scopeProceedings of the 21st European conference on Programming Languages and Systems10.1007/978-3-642-28869-2_28(559-578)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28869-2_28
Westbrook EFrisby NBrauner P(2011)Hobbits for HaskellACM SIGPLAN Notices10.1145/2096148.203468146:12(35-46)Online publication date: 22-Sep-2011
https://dl.acm.org/doi/10.1145/2096148.2034681
Westbrook EFrisby NBrauner PClaessen K(2011)Hobbits for HaskellProceedings of the 4th ACM symposium on Haskell10.1145/2034675.2034681(35-46)Online publication date: 22-Sep-2011
https://dl.acm.org/doi/10.1145/2034675.2034681
Choi WAktemur BYi KTatsuta MBall TSagiv M(2011)Static analysis of multi-staged programs via unstaging translationProceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1926385.1926397(81-92)Online publication date: 26-Jan-2011
https://dl.acm.org/doi/10.1145/1926385.1926397
Choi WAktemur BYi KTatsuta M(2011)Static analysis of multi-staged programs via unstaging translationACM SIGPLAN Notices10.1145/1925844.192639746:1(81-92)Online publication date: 26-Jan-2011
https://dl.acm.org/doi/10.1145/1925844.1926397
Liu YSkalka CSmith S(2011)Type-specialized staged programming with process separationHigher-Order and Symbolic Computation10.1007/s10990-012-9089-024:4(341-385)Online publication date: 1-Nov-2011
https://dl.acm.org/doi/10.1007/s10990-012-9089-0
Rompf TOdersky M(2010)Lightweight modular stagingACM SIGPLAN Notices10.1145/1942788.186831446:2(127-136)Online publication date: 10-Oct-2010
https://dl.acm.org/doi/10.1145/1942788.1868314
Rompf TOdersky MVisser EJärvi J(2010)Lightweight modular stagingProceedings of the ninth international conference on Generative programming and component engineering10.1145/1868294.1868314(127-136)Online publication date: 10-Oct-2010
https://dl.acm.org/doi/10.1145/1868294.1868314
Westbrook ERicken MInoue JYao YAbdelatif TTaha W(2010)MintACM SIGPLAN Notices10.1145/1809028.180664245:6(400-411)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1809028.1806642
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents