Static analysis of multi-staged programs via unstaging translation. (English) Zbl 1284.68170
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’11, Austin, TX, USA, January 26–28, 2011. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-0490-0). 81-92 (2011).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
Keywords:
abstract interpretation; multi-staged language; projection; semantics perservation; static analysis; unstaging translationReferences:
| [1] | Baris Aktemur. Improving Efficiency and Safety of Program Generation. PhD thesis, University of Illinois at Urbana-Champaign, 2009. |
| [2] | Martin Berger and Laurence Tratt. Program logics for homogeneous meta-programming. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, to appear, 2010. |
| [3] | Cristiano Calcagno, Eugenio Moggi, and Walid Taha. Closed types as a simple approach to safe imperative multi-stage programming. In ICALP ’00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming, pages 25-36, London, UK, 2000. Springer-Verlag. · Zbl 0973.68037 |
| [4] | Chiyan Chen and Hongwei Xi. Meta-programming through typeful code representation. In ACM International Conference on Functional Programming, pages 275-286. ACM, August 2003. 10.1145/944705.944730 · Zbl 1315.68038 |
| [5] | Tae-Hyoung Choi, Oukseh Lee, Hyunha Kim, and Kyung-Goo Doh. A practical string analyzer by the widening approach. In Proceedings of the Asian Symposium on Programming Languages and Systems, volume 4729 of Lecture Notes in Computer Science, pages 374-388, Sydney, Austrailia, November 2006. Springer-Verlag. 10.1007/11924661_23 · Zbl 1168.68359 |
| [6] | Wontae Choi, Baris Aktemur, and Kwangkeun Yi. Semantics preservation proof of an unstaging translation of lisp-like multi-staged languages. Technical Report ROSAEC-2010-009, ROSAEC Center, Seoul National University, 2010. http://rosaec.snu.ac.kr/publish/2010/techmemo/ROSAEC-2010-009.pdf. |
| [7] | Aske Simon Christensen, Anders Muller, and Michael I. Schwartzbach. Precise analysis of string expressions. In Proceedings of the Static Analysis Symposium, pages 1-18. Springer-Verlag, 2003. · Zbl 1067.68541 |
| [8] | Hubert Comon, Max Dauchet, Remi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications, April 1999. |
| [9] | P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238-252, Los Angeles, California, 1977. ACM Press, New York, NY. 10.1145/512950.512973 |
| [10] | P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511-547, 1992. · Zbl 0783.68073 |
| [11] | Patrick Cousot and Radhia Cousot. Systematic design of program transformation frameworks by abstract interpretation. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages pp.178-190, January 2002. 10.1145/503272.503290 · Zbl 1323.68356 |
| [12] | Olivier Danvy. Type-directed partial evaluation. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 242-257. ACM, Jan 1996. 10.1145/237721.237784 |
| [13] | Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 258-270. ACM, 1996. 10.1145/237721.237788 |
| [14] | Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555-604, 2001. 10.1145/382780.382785 · Zbl 1323.68107 |
| [15] | Kyung-Goo Doh, Hyunha Kim, and David Schmidt. Abstract parsing: static analysis of dynamically generated string output using LR-parsing technology. In Proceeeding of the International Static Analysis Symposium, 2009. 10.1007/978-3-642-03237-0_18 |
| [16] | Dawson R. Engler. VCODE:A retargetable, extensible, very fast dynamic code generation system. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, pages 160-170, New York, 1996. ACM. 10.1145/231379.231411 |
| [17] | Ferenc Gécseg and Magnus Steinby. Tree Automata. Akadémiai Kiadó, 1984. · Zbl 0537.68056 |
| [18] | Paul Graham. On Lisp: an advanced techniques for Common Lisp. Prentice Hall, 1994. |
| [19] | Nevin Heintze. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, October 1992. |
| [20] | Nevin Heintze. Set based analysis of ML programs. In Proceedings of the SIGPLAN Conference on Lisp and Functional Programming, pages 306-317, 1994. 10.1145/182409.182495 |
| [21] | Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial evaluation and automatic program generation. Prentice-Hall, 1993. · Zbl 0875.68290 |
| [22] | Pierre Jouvelot and David K. Gifford. Algebraic reconstruction of types and effects. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 303-310, 1991. 10.1145/99583.99623 |
| [23] | Yukiyoshi Kameyama, Oleg Kiselyov, and Chung chieh Shan. Closing the stage: from staged code to typed closure. In Proceedings of The ACM Symposium on Partial Evaluation and Program Manipulations, pages 147-157, 2008. 10.1145/1328408.1328430 |
| [24] | Sam Kamin, Baris Aktemur, and Michael Katelman. Staging static analyses for program generation. In GPCE ’06: Proceedings of the 5th international conference on Generative programming and component engineering, pages 1-10, New York, NY, USA, 2006. ACM. 10.1145/1173706.1173708 |
| [25] | Ik-Soon Kim, Kwangkeun Yi, and Cristiano Calcagno. A polymorphic modal type system for lisp-like multi-staged languages. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 257-269, 2006. 10.1145/1111037.1111060 · Zbl 1369.68076 |
| [26] | M. Leone and Peter Lee. Optimizing ML with run-time code generation. In Proceedings of the ACM SIGPLAN’96 Conference on Programming Language Design and Implementation, pages 137-148. ACM Press, June 1996. 10.1145/231379.231407 |
| [27] | John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 47-57, 1988. 10.1145/73560.73564 |
| [28] | H. Massalim. An Efficient Implementation of Functional Operating System Services. PhD thesis, Columbia University, 1992. |
| [29] | Yasuhiko Minamide. Static approximation of dynamically generated web pages. In Proceedings of the International Conference on World Wide Web, pages 432-441, New York, NY, USA, 2005. ACM. 10.1145/1060745.1060809 |
| [30] | Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 271-283. ACM, 1996. 10.1145/237721.237791 |
| [31] | Aleksandar Nanevski and Frank Pfenning. Staged computation with names and necessity. Journal of Functional Programming, 15(6):893-939, 2005. 10.1017/S095679680500568X · Zbl 1085.68025 |
| [32] | Massimilian Poletto, Wilson C. Hsieh, Dawson R. Engler, and M. Frans Kasshoek. C and tcc:a language and compiler for dynamic code generation. ACM Transactions on Programming Languages and Systems, 21:324-369, March 1999. 10.1145/316686.316697 |
| [33] | Tim Sheard and Simon Peyton Jones. Template meta-programming for Haskell. In Proceedings of The Haskell Workshop, October 2002. http:/www.haskell.org/haskellwiki/Template_Haskell 10.1145/581690.581691 |
| [34] | Frederick Smith, Dan Grossman, Greg Morrisett, Luke Hornof, and Trevor Jim. Compiling for template-based run-time code generation. Journal of Functional Programming, 13(3):677-708, 2003. 10.1017/S095679680200463X · Zbl 1036.68019 |
| [35] | Guy L. Steele. Common Lisp the Language, 2nd edition. Digital Press, 1990. · Zbl 0757.68008 |
| [36] | Walid Taha, Cristiano Calcagno, Xavier Leroy, and Ed Pizzi. MetaOCaml. http:/www.metaocaml.org/ |
| [37] | Walid Taha and Michael Florentin Nielsen. Environment classifiers. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 2003. 10.1145/604131.604134 · Zbl 1321.68175 |
| [38] | Makoto Tatsuta. Translation of multi-staged language. Technical Report NII-2010-003E, National Institute of Informatics, Tokyo, 2010. http://research.nii.ac.jp/TechReports. |
| [39] | Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 188-201, January 1994. 10.1145/174675.177855 |
| [40] | Edwin Westbrook, Mathias Ricken, Jun Inoue, Yilong Yao, Tamer Abdelatif, and Walid Taha. Mint: Java multi-stage programming using weak separability. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010. 10.1145/1806596.1806642 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
