Environment classifiers. (English) Zbl 1321.68175
Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’03, New Orleans, LA, USA, January 15–17, 2003. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-628-5). 26-37 (2003).
MSC:
| 68N19 | Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) |
| 03B70 | Logic in computer science |
| 68N15 | Theory of programming languages |
Software:
TREXReferences:
| [1] | Martín Abadi, Luca Cardelli, and Pierre-Louis Curien. Formal parametric polymorphism. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 157-170. ACM New York, NY, 1993.]] 10.1145/158511.158622 |
| [2] | Joel Auslander, Matthai Philipose, Craig Chambers, Susan J. Eggers, and Brian N. Bershad. Fast, effective dynamic compilation. In Proceedings of the Conference on Programming Language Design and Implementation, pages 149-159, Philadelphia, 1996.]] 10.1145/231379.231409 |
| [3] | Don Batory. Refinements and product line architectures. In {61}, pages 3-4, 2000.]] |
| [4] | Zine-El-Abidine Benaissa, Daniel Briaud, Pierre Lescanne, and Jocelyne Rouyer-Degli. λv, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming, 6(5):699-722, 1996.]] · Zbl 0873.68108 |
| [5] | 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), 1999.]] |
| [6] | Cristiano Calcagno and Eugenio Moggi. Multi-stage imperative languages: A conservative extension result. In {61}, pages 92-107, 2000.]] · Zbl 1044.68025 |
| [7] | Cristiano Calcagno, Eugenio Moggi, and Tim Sheard. Closed types for a safe imperative MetaML. Journal of Functional Programming, 2003. To appear.]] 10.1017/S0956796802004598 · Zbl 1036.68024 |
| [8] | Cristiano Calcagno, Eugenio Moggi, and Walid Taha. Closed types as a simple approach to safe imperative multi-stage programming. In the International Colloquium on Automata, Languages, and Programming (ICALP ’00), volume 1853 of Lecture Notes in Computer Science, pages 25-36, Geneva, 2000. Springer-Verlag.]] · Zbl 0973.68037 |
| [9] | Luca Cardelli. Program fragments, linking, and modularization. In Conference Record of POPL ’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 266-277, Paris, France, 15-17 January 1997.]] 10.1145/263699.263735 |
| [10] | Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In ACM Symposium on Principles of Programming Languages, pages 493-501, 1993.]] 10.1145/158511.158707 |
| [11] | Charles Consel, Calton Pu, and Jonathan Walpole. Incremental partial evaluation: The key to high performance, modularity and portability in OPerating systems. In Partial Evaluation and Semantics-Based Program Manipulation, Copenhagen, Denmark, June 1993, pages 44-46. ACM, 1993.]] 10.1145/154630.154635 |
| [12] | Luís Damas and Robin Milner. Principal type schemes for functional languages. In 9th ACM Symposium on Principles of Programming Languages. ACM, August 1982.]] 10.1145/582153.582176 |
| [13] | Olivier Danvy, Karoline Malmkjaer, and Jens Palsberg. Eta-expansion does the trick. Technical Report RS-95-41, University of Aarhus, Aarhus, 1995.]] |
| [14] | Rowan Davies. A temporal-logic approach to binding-time analysis. In the Symposium on Logic in Computer Science (LICS ’96), pages 184-195, New Brunswick, 1996. IEEE Computer Society Press.]] |
| [15] | Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In the Symposium on Principles of Programming Languages (POPL ’96), pages 258-270, St. Petersburg Beach, 1996.]] 10.1145/237721.237788 |
| [16] | 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 |
| [17] | Dawson R. Engler. VCODE : A retargetable, extensible, very fast dynamic code generation system. In Proceedings of the Conference on Programming Language Design and Implemantation, pages 160-170, New York, 1996. ACM.]] 10.1145/231379.231411 |
| [18] | Dawson R. Engler, Wilson C. Hsieh, and M. Frans Kaashoek. ’C: A language for high-level, efficient, and machine-independent dynaic code generation. In In proceedings of the ACM Symposium on Principles of Programming Languages (POPL), pages 131-144, St. Petersburg Beach, 1996.]] 10.1145/237721.237765 |
| [19] | Adam Fischbach and John Hannan. Specification and correctness of lambda lifting. In {61}, pages 108-128, 2000.]] · Zbl 1044.68027 |
| [20] | Yoshihiko Futamura. Partial evaluation of computation process – an approach to a compiler-compiler. Systems, Computers and Control, 2(5):45-50, 1971. {Via {33}}.]] |
| [21] | Steven Ganz, Amr Sabry, and Walid Taha. Macros as multi-stage computations: Type-safe, generative, binding macros in MacroML. In the International Conference on Functional Programming (ICFP ’01), Florence, Italy, September 2001. ACM.]] 10.1145/507635.507646 · Zbl 1323.68116 |
| [22] | Garrigue and Remy. Semi-explicit first-class polymorphism for ML. INFCTRL: Information and Computation (formerly Information and Control), 155, 1999.]] 10.1006/inco.1999.2830 |
| [23] | Robert Glück and Jesper Jθrgensen. Efficient multi-level generating extensions for program specialization. In S. D. Swierstra and M. Hermenegildo, editors, Programming Languages: Implementations, Logics and Programs (PLILP’95), volume 982 of Lecture Notes in Computer Science, pages 259-278. Springer-Verlag, 1995.]] |
| [24] | 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.]] |
| [25] | Robert Glück and Jesper Jθrgensen. An automatic program generator for multi-level specialization. LISP and Symbolic Computation, 10(2):113-158, 1997.]] 10.1023/A:1007763000430 |
| [26] | Carsten K. Gomard. Partial type inference for untyped functional programs. In ACM Conference on Lisp and Functional Programming, 1990.]] 10.1145/91556.91672 |
| [27] | Carsten K. Gomard and Neil D. Jones. A partial evaluator for untyped lambda calculus. Journal of Functional Programming, 1(1):21-69, 1991.]] · Zbl 1155.68350 |
| [28] | Brian Grant, Markus Mock, Matthai Philipose, Craig Chambers, and Susan J. Eggers. Annotation-directed run-time specialization in C. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 163-178, Amsterdam, 1997.]] 10.1145/258993.259016 |
| [29] | Brian Grant, Matthai Philipose, Markus Mock, Craig Chambers, and Susan J. Eggers. An evaluation of staged run-time optimizations in DyC. In Proceedings of the Conference on Programming Language Design and Implementation, pages 293-304, 1999.]] 10.1145/301618.301683 |
| [30] | Torben Amtoft Hansen, Thomas Nikolajsen, Jesper Larsson Träff, and Neil D. Jones. Experiments with implementations of two theoretical constructions. In Lecture Notes in Computer Science 363, pages 119-133. Springer Verlag, 1989.]] · Zbl 0673.03035 |
| [31] | J. Roger Hindley. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1997.]] · Zbl 0906.03012 |
| [32] | N. D. Jones, P. Sestoft, and H. Søndergaard. An experiment in partial evaluation: the generation of a compiler generator. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, Dijon, France, volume 202 of Lecture Notes in Computer Science, pages 124-140. Springer-Verlag, 1985.]] |
| [33] | Neil D. Jones. Mix ten years later. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 24-38. ACM, 1995.]] 10.1145/215465.215468 |
| [34] | Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.]] · Zbl 0875.68290 |
| [35] | Neil D. Jones, Peter Sestoft, and Harald Sondergraard. An experiment in partial evaluation: The generation of a compiler generator. In Jean-Pierre Jouannaud, editor, Rewriting Techniques and Applications, volume 202 of Lecture Notes in Computer Science, pages 124-140. Springer-Verlag, 1985.]] |
| [36] | Sam Kamin, Miranda Callahan, and Lars Clausen. Lightweight and generative components II: Binary-level components. In {61}, pages 28-50, 2000.]] · Zbl 1044.68529 |
| [37] | John Launchbury and Simon L. Peyton Jones. State in haskell. LISP and Symbolic Computation, 8(4):293-342, 1995. pldi94.]] 10.1007/BF01018827 |
| [38] | Jeffrey R. Lewis, John Launchbury, Erik Meijer, and Mark Shields. Implicit parameters: Dynamic scoping with static types. In In proceedings of the ACM Symposium on Principles of Programming Languages (POPL), pages 108-118, N.Y., January 19-21 2000. ACM.]] 10.1145/325694.325708 · Zbl 1323.68131 |
| [39] | MetaOCaml: A compiled, type-safe multi-stage programming language. Available online from http://cs-www.cs.yale.edu/homes/taha/MetaOCaml/, 2001.]] |
| [40] | Eugenio Moggi. Functor categories and two-level languages. In Foundations of Software Science and Computation Structures (FoSSaCS), volume 1378 of Lecture Notes in Computer Science. Springer Verlag, 1998.]] · Zbl 0904.03017 |
| [41] | Eugenio Moggi and Amr Sabry. Monadic encapsulation of effects. Journal of Functional Programming, 2001.]] 10.1017/S0956796801004154 |
| [42] | 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.]] |
| [43] | Aleksander Nanevski. Meta-programming with names and necessity. In the International Conference on Functional Programming (ICFP ’02), Pittsburgh, USA, October 2002. ACM.]] 10.1145/581478.581498 · Zbl 1322.68045 |
| [44] | Flemming Nielson. Program transformations in a denotational setting. ACM Transactions on Programming Languages and Systems, 7(3):359-379, 1985.]] 10.1145/3916.3917 · Zbl 0566.68013 |
| [45] | Flemming Nielson. Correctness of code generation from a two-level meta-language. In B. Robinet and R. Wilhelm, editors, Proceedings of the European Symposium on Programming (ESOP 86), volume 213 of Lecture Notes in Computer Science, pages 30-40, Saarbrücken, 1986. Springer.]] · Zbl 0589.68012 |
| [46] | 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.]] |
| [47] | Flemming Nielson and Hanne Riis Nielson. Two-level semantics and code generation. Theoretical Computer Science, 56(1):59-133, 1988.]] 10.1016/0304-3975(86)90006-X · Zbl 0632.68007 |
| [48] | Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages. Number 34 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1992.]] |
| [49] | Flemming Nielson and Hanne Riis Nielson. Multi-level lambda-calculi: An algebraic description. In O. Danvy, R. Glück, and P. Thiemann, editors, Partial Evaluation. Dagstuhl Castle, Germany, February 1996, volume 1110 of Lecture Notes in Computer Science, pages 338-354. Berlin: Springer-Verlag, 1996.]] |
| [50] | Flemming Nielson and Hanne Riis Nielson. A prescriptive framework for designing multi-level lambda-calculi. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 193-202, Amsterdam, 1997. ACM.]] 10.1145/258993.259018 |
| [51] | Hanne Riis Nielson and Flemming Nielson. Automatic binding time analysis for a typed λ-calculus. In ACM Symposium on Principles of Programming Languages, pages 98-106, 1988.]] 10.1145/73560.73569 |
| [52] | Françcois Noël, Luke Hornof, Charles Consel, and Julia L. Lawall. Automatic, template-based run-time specialization: Implementation and experimental study. In Proceedings of the 1998 International Conference on Computer Languages, pages 132-142. IEEE Computer Society Press, 1998.]] |
| [53] | Oregon Graduate Institute Technical Reports. P.O. Box 91000, Portland, OR 97291-1000,USA. Available online from ftp://cse.ogi.edu/pub/tech-reports/README.html. Last viewed August 1999.]] |
| [54] | Emir PašaliΕ, Walid Taha, and Tim Sheard. Tagless staged interpreters for typed languages. In the International Conference on Functional Programming (ICFP ’02), Pittsburgh, USA, October 2002. ACM.]] 10.1145/581478.581499 · Zbl 1322.68033 |
| [55] | Andrew M. Pitts and Murdoch J. Gabbay. A metalanguage for programming with bound names modulo renaming. In Mathematics of Programme Construction, volume 1837 of Lecture Notes in Computer Science, pages 230-255. Springer-Verlag, 2000.]] · Zbl 0963.68502 |
| [56] | John C. Reynolds. Towards a theory of types structure. In Proceedings Colloque sur la Programmation, pages 408-423. Springer-Verlag, New York, 1974.]] |
| [57] | Claudio Russo. Types for Modules. PhD thesis, Edinburgh University, 1998.]] |
| [58] | Mark Shields, Tim Sheard, and Simon L. Peyton Jones. Dynamic typing through staged type inference. In In proceedings of the ACM Symposium on Principles of Programming Languages (POPL), pages 289-302, 1998.]] 10.1145/268946.268970 |
| [59] | Yannis Smaragdakis and Don Batory. DiSTiL: A transformation library for data structures. In USENIX Conference on Domain-Specific Languages, 1997.]] |
| [60] | Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, 1999. Available from {53}.]] |
| [61] | Walid Taha, editor. Semantics, Applications, and Implementation of Program Generation, volume 1924 of Lecture Notes in Computer Science, Montréal, 2000. Springer-Verlag.]] · Zbl 0947.00043 |
| [62] | Walid Taha. A sound reduction semantics for untyped CBN multi-stage computation. Or, the theory of MetaML is non-trivial. In Proceedings of the Workshop on Partial Evaluation and Semantics-Based Program Maniplation (PEPM), Boston, 2000. ACM.]] 10.1145/328690.328697 |
| [63] | 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 (ICALP), volume 1443 of Lecture Notes in Computer Science, pages 918-929, Aalborg, 1998.]] |
| [64] | Walid Taha and Tim Sheard. Multi-stage programming with explicit annotations. In Proceedings of the Symposium on Partial Evaluation and Semantic-Based Program Manipulation (PEPM), pages 203-217, Amsterdam, 1997. ACM.]] 10.1145/258993.259019 |
| [65] | Philip Wadler. Theorems for free! In Proc. of 4th Int. Conf. on Funct. Prog. Languages and Computer Arch., FPCA’89, London, UK, 11-13 Sept. 1989, pages 347-359. ACM, New York, 1989.]] 10.1145/99370.99404 |
| [66] | Mitchell Wand. Complete type inference for simple objects. In Second Annual IEEE Symp. on Logic in Computer Science, 1987.]] |
| [67] | Mitchell Wand. The theory of fexprs is trivial. Lisp and Symbolic Computation, 10:189-199, 1998.]] 10.1023/A:1007720632734 |
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.
