Environment classifiers

ABSTRACT

This paper proposes and develops the basic theory for a new approach to typing multi-stage languages based a notion of environment classifiers. This approach involves explicit but lightweight tracking -- at type-checking time -- of the origination environment for future-stage computations. Classification is less restrictive than the previously proposed notions of closedness, and allows for both a more expressive typing of the "run" construct and for a unifying account of typed multi-stage programmin.The proposed approach to typing requires making cross-stage persistence (CSP) explicit in the language. At the same time, it offers concrete new insights into the notion of levels and in turn into CSP itself. Type safety is established in the simply-typed setting. As a first step toward introducing classifiers to the Hindley-Milner setting, we propose an approach to integrating the two, and prove type preservation in this setting.

REFERENCES

• 1: Martín Abadi , Luca Cardelli , Pierre-Louis Curien, Formal parametric polymorphism, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.157-170, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158622]
• 2: Joel Auslander , Matthai Philipose , Craig Chambers , Susan J. Eggers , Brian N. Bershad, Fast, effective dynamic compilation, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.149-159, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 3: Don S. Batory, Refinements and Product Line Architectures, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, p.3-4, September 20, 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.
• 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 , Eugenio Moggi, Multi-Stage Imperative Languages: A Conservative Extension Result, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, p.92-107, September 20, 2000
• 7: C. Calcagno , E. Moggi , T. Sheard, Closed types for a safe imperative MetaML, Journal of Functional Programming, v.13 n.3, p.545-571, May 2003 [doi>10.1017/S0956796802004598]
• 8: Cristiano Calcagno , Eugenio Moggi , Walid Taha, Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, p.25-36, July 09-15, 2000
• 9: Luca Cardelli, Program fragments, linking, and modularization, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.266-277, January 15-17, 1997, Paris, France [doi>10.1145/263699.263735]
• 10: Charles Consel , Olivier Danvy, Tutorial notes on partial evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.493-501, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158707]
• 11: Charles Consel , Calton Pu , Jonathan Walpole, Incremental partial evaluation: the key to high performance, modularity and portability in operating systems, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.44-46, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154635]
• 12: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>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: R. Davies, A temporal-logic approach to binding-time analysis, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.184, July 27-30, 1996
• 15: Rowan Davies , Frank Pfenning, A modal analysis of staged computation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.258-270, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237788]
• 16: Rowan Davies , Frank Pfenning, A modal analysis of staged computation, Journal of the ACM (JACM), v.48 n.3, p.555-604, May 2001 [doi>10.1145/382780.382785]
• 17: Dawson R. Engler, VCODE: a retargetable, extensible, very fast dynamic code generation system, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.160-170, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 18: Dawson R. Engler , Wilson C. Hsieh , M. Frans Kaashoek, C: a language for high-level, efficient, and machine-independent dynamic code generation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.131-144, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237765]
• 19: Adam Fischbach , John Hannan, Specification and Correctness of Lambda Lifting, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, p.108-128, September 20, 2000
• 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 E. Ganz , Amr Sabry , Walid Taha, Macros as multi-stage computations: type-safe, generative, binding macros in MacroML, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 22: Jacques Garrigue , Didier Rémy, Semi-explicit first-class polymorphism for ML, Information and Computation, v.155 n.1-2, p.134-169, Nov./Dec. 1999 [doi>10.1006/inco.1999.2830]
• 23: Robert Glück , Jesper Jørgensen, Efficient Multi-level Generating Extensions for Program Specialization, Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs, p.259-278, September 20-22, 1995
• 24: Robert Glück , Jesper Jørgensen, Fast Binding-Time Analysis for Multi-Level Specialization, Proceedings of the Second International Andrei Ershov Memorial Conference on Perspectives of System Informatics, p.261-272, June 25-28, 1996
• 25: Robert Glück , Jesper Jørgensen, An Automatic Program Generator for Multi-Level Specialization, Lisp and Symbolic Computation, v.10 n.2, p.113-158, July 1997 [doi>10.1023/A:1007763000430]
• 26: Carsten K. Gomard, Partial type inference for untyped functional programs, Proceedings of the 1990 ACM conference on LISP and functional programming, p.282-287, June 27-29, 1990, Nice, France [doi>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.
• 28: Brian Grant , Markus Mock , Matthai Philipose , Craig Chambers , Susan J. Eggers, Annotation-directed run-time specialization in C, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.163-178, June 12-13, 1997, Amsterdam, The Netherlands
• 29: Brian Grant , Matthai Philipose , Markus Mock , Craig Chambers , Susan J. Eggers, An evaluation of staged run-time optimizations in DyC, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.293-304, May 01-04, 1999, Atlanta, Georgia, United States
• 30: Torben Amtoft Hansen , Thomas Nikolajsen , Jesper Larsson Träff , Neil D. Jones, Experiments with Implementations of Two Theoretical Constructions, Proceedings of the Symposium on Logical Foundations of Computer Science: Logic at Botik '89, p.119-133, July 03-08, 1989
• 31: J. Roger Hindley, Basic simple type theory, Cambridge University Press, New York, NY, 1997
• 32: Neil D. Jones , Peter Sestoft , Harald Sondergaard, An experiment in partial evaluation: the generation of a compiler generator, Proc. of the first international conference on Rewriting techniques and applications, p.124-140, December 1985, Dijon, France
• 33: Neil D. Jones, Mix ten years later, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.24-38, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215468]
• 34: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 35: Neil D. Jones , Peter Sestoft , Harald Sondergaard, An experiment in partial evaluation: the generation of a compiler generator, Proc. of the first international conference on Rewriting techniques and applications, p.124-140, December 1985, Dijon, France
• 36: Samuel N. Kamin , Miranda Callahan , Lars Clausen, Lightweight and Generative Components 2: Binary-Level Components, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, p.28-50, September 20, 2000
• 37: John Launchbury , Simon L. Peyton Jones, State in Haskell, Lisp and Symbolic Computation, v.8 n.4, p.293-341, Dec. 1995 [doi>10.1007/BF01018827]
• 38: Jeffrey R. Lewis , John Launchbury , Erik Meijer , Mark B. Shields, Implicit parameters: dynamic scoping with static types, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.108-118, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325708]
• 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, Proceedings of the First International Conference on Foundations of Software Science and Computation Structure, p.211-225, March 28-April 04, 1998
• 41: E. Moggi , Amr Sabry, Monadic encapsulation of effects: a revised approach (extended version), Journal of Functional Programming, v.11 n.6, p.591-627, November 2001 [doi>10.1017/S0956796801004154]
• 42: Eugenio Moggi , Walid Taha , Zine-El-Abidine Benaissa , Tim Sheard, An Idealized MetaML: Simpler, and More Expressive, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.193-207, March 22-28, 1999
• 43: Aleksandar Nanevski, Meta-programming with names and necessity, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.206-217, October 04-06, 2002, Pittsburgh, PA, USA
• 44: Flemming Nielson, Program transformations in a denotational setting, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.359-379, July 1985 [doi>10.1145/3916.3917]
• 45: F Nielson, Correctness of code generation from a two-level meta-language, Proc. of the European symposium on programming on ESOP 86, p.30-40, March 1986, Saarbru:9Aicken, Germany
• 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 , Hanne Riis Nielson, Two-level semantics and code generation, Theoretical Computer Science, v.56 n.1, p.59-133, Jan. 1988 [doi>10.1016/0304-3975(86)90006-X]
• 48: Flemming Nielson , Hanne Riis Nielson, Two-level functional languages, Cambridge University Press, New York, NY, 1992
• 49: Flemming Nielson , Hanne Riis Nielson, Multi-Level Lambda-Calculi: An Algebraic Description, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.338-354, February 12-16, 1996
• 50: Flemming Nielson , Hanne Riis Nielson, Prescriptive frameworks for multi-level lambda-calculi, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.193-202, June 12-13, 1997, Amsterdam, The Netherlands
• 51: F. Nielson , R. H. Nielson, Automatic binding time analysis for a typed &lgr;-calculus, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-106, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73569]
• 52: Francois Noel , Luke Hornof , Charles Consel , Julia L. Lawall, Automatic, Template-Based Run-Time Specialization: Implementation and Experimental Study, Proceedings of the 1998 International Conference on Computer Languages, p.132, May 14-16, 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 , Tim Sheard, Tagless staged interpreters for typed languages, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.218-229, October 04-06, 2002, Pittsburgh, PA, USA
• 55: Andrew M. Pitts , Murdoch Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.230-255, July 03-05, 2000
• 56: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 57: Claudio Russo. Types for Modules. PhD thesis, Edinburgh University, 1998.
• 58: Mark Shields , Tim Sheard , Simon Peyton Jones, Dynamic typing as staged type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.289-302, January 19-21, 1998, San Diego, California, United States [doi>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 Mohamed Taha , Tim Sheard, Multistage programming: its theory and applications, 1999
• 61: Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, September 2000
• 62: Walid Taha, A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trival (extended abstract), Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.34-43, January 22-23, 2000, Boston, Massachusetts, United States
• 63: Walid Taha , Zine-El-Abidine Benaissa , Tim Sheard, Multi-Stage Programming: Axiomatization and Type Safety, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.918-929, July 13-17, 1998
• 64: Walid Taha , Tim Sheard, Multi-stage programming with explicit annotations, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.203-217, June 12-13, 1997, Amsterdam, The Netherlands
• 65: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>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, v.10 n.3, p.189-199, May 1998 [doi>10.1023/A:1007720632734]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs

General Terms:
Design, Languages, Reliability, Theory, Verification

Keywords:
linear temporal logic, modal logic, multi-stage programming, type safety, type systems