Implementing Typeful Program Transformations

• Autorzy: Chen Ch. , Shi R. , Xi H.
• Języki publikacji: EN

Abstrakty

EN

The notion of program transformation is ubiquitous in programming language studies on interpreters, compilers, partial evaluators, etc. In order to implement a program transformation, we need to choose a representation in the meta language, that is, the programming language in which we construct programs, for representing object programs, that is, the programs in the object language on which the program transformation is to be performed. In practice, most representations chosen for typed object programs are typeless in the sense that the type of an object program cannot be reflected in the type of its representation. This is unsatisfactory as such typeless representations make it impossible to capture in the type system of the meta language various invariants in a program transformation that are related to the types of object programs. In this paper, we propose an approach to implementing program transformations that makes use of a first-order typeful program representation, where the type of an object program as well as the types of the free variables in the object program can be reflected in the type of the representation of the object program. We introduce some programming techniques needed to handle this typeful program representation, and then present an implementation of a CPS transform function where the relation between the type of an object program and that of its CPS transform is captured in the type system of DML. In a broader context, we claim to have taken a solid step along the line of research on constructing certifying compilers.

Słowa kluczowe

EN

typeful program transformation; dependent types; Applied Type System; ATS; Continuation Passing Style; CPS; closure conversion

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 69, nr 1,2
• Strony: 103--103
• Opis fizyczny: 121, bibliogr. 34 poz.

Twórcy

autor

Chen Ch.

autor

Shi R.

autor

Xi H.

• Computer Science Deprtment Boston University Boston MA 02215, USA,

Bibliografia

• [1] Abadi,M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit Substitutions, Journal of Functional Programming, 1(4), 1991, 375-416.
• [2] Augustsson, L.: Cayenne - a language with dependent types, Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming, Baltimore, 1998.
• [3] Augustsson, L., Carlsson, M.: An excercise in dependent types: A well-typed interpreter, Available at http://www.cs.chalmers.se/~augustss/cayenne/interp.ps, 1999
• [4] de Bruijn, N. G.: Lambda calculus notation with nameless dummies, Indagationes mathematicae, 34, 1972, 381-392.
• [5] Cardelli, L.: Typeful Programming, in: Formal Description of Programming Concepts (E. J. Neuhold, M. Paul, Eds.), Springer-Verlag, Berlin, 1991, 431-507.
• [6] Chen, C., Xi, H.: Implementing Typeful ProgramTransformations, Proceedings of ACMSIGPLANWorkshop on Partial Evaluation and Semantics Based Program Manipulation, San Diego, CA, June 2003.
• [7] Chen, C., Xi, H.: Combining Programming with Theorem Proving, November 2004, Available at:http://www.cs.bu.edu/~hwxi/ATS/PAPER/CPwTP.ps
• [8] Chen, C., Zhu, D., Xi, H.: Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell, Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages, Springer-Verlag LNCS vol. 3057, Dallas, TX, June 2004.
• [9] Cheney, J., Hinze, R.: Phantom Types, Technical Report CUCIS-TR2003-1901, Cornell University, 2003, Available at http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Displey/cul.cis
• [10] Danvy, O., Rhiger, M., Rose, K.: Normalization by Evaluation with Typed Abstract Syntax, Journal of Functional Programming, 11(6), 2001, 673-680.
• [11] Griffin, T.: A Formulae-as-Types Notion of Control, Conference Record of POPL '90: 17th ACM SIGPLAN Symposium on Principles of Programming Languages, San Francisco, CA, January 1990.
• [12] Harper, R. W., Honsell, F., Plotkin, G. D.: A Framework for Defining Logics, Journal of the ACM, 40(1), January 1993, 143-184.
• [13] Hinze, R.: Fun with Phantom Types, in: The Fun of Programming (J. Gibbons, O. de Moor, Eds.), Palgrave Macmillan, 2003, ISBN 1-4039-0772-2 (hardback) 0-333-99285-7 (paperback), 245-262.
• [14] Meyer, A., Wand, M.: Continuation Semantics in Typed Lambda Calculi (summary), Logics of Programs (R. Parikh, Ed.), Springer-Verlag LNCS 224, 1985.
• [15] Milner, R., Tofte, M., Harper, R. W., MacQueen, D.: The Definition of Standard ML (Revised), MIT Press, Cambridge,Massachusetts, 1997, ISBN 0-262-63181-4.
• [16] Minamide, Y., Morrisett, G., Harper, R.: Typed closure conversion, Proceedings of 23rd Annual ACM Symposium on Principles of Programming Languages (POPL '96), St. Petersburgh, Florida, 1996.
• [17] Minamide, Y., Okuma, K.: Verifying CPS transformations in Isabelle/HOL, Proceedings of Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN), 2003.
• [18] Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to Typed Assembly Language, ACM Transactions on Programming Languages and Systems, 21(3),May 1999, 527-568.
• [19] Nanevski, A., Pfenning, F.: Meta-Programming with Names and Necessity, To appear in JFP. A previous version appeared in the Proceedings of the International Conference on Functional Programming (ICFP 2002), pp. 206-217.
• [20] Pasalic, E., Linger, N.: Meta-programming with Typed Object-Language Representations., The 3rd International Conference on Generative Programming and Component Engineering (GPCE'04) (G. Karsai, E. Visser, Eds.), Springer-Verlag LNCS, 3286, Vancouver, BC, 2004.
• [21] Pasalic, E.,Walid Taha, T. S.: Tagless Staged Interpreters for Typed Languages, Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, PA, October 2002.
• [22] Peyton Jones, S., et al.: Haskell 98 - A Non-strict, Purely Functional Language, Available at http://haskell.org.onlinereport/, February 1999.
• [23] Pfenning, F., Elliott, C.: Higher-order abstract syntax, Proceedings of the ACM SIGPLAN '88 Symposium on Language Design and Implementation, Atlanta, Georgia, June 1988.
• [24] Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems, Proceedings of the 16th International Conference on Automated Deduction (CADE-16) (H. Ganzinger, Ed.), Springer-Verlag LNAI 1632, Trento, Italy, July 1999.
• [25] Pitts, A. M.: Nominal Logic, A First Order Theory of Names and Binding, Information and Computation, 186(2), November 2003, 165-193.
• [26] Plotkin, G. D.: Call-by-Name, Call-by-Value and the λ-Calculus, Theoretical Computer Science, 1(2), December 1975, 125-159.
• [27] Tarditi, D.,Morrisett, G., Cheng, P., Stone, C., Harper, R., Lee, P.: A Type-Directed Optimizing Compiler for ML, Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, June 1996.
• [28] Xi, H.: Dependent Types in Practical Programming, Ph.D. Thesis, Carnegie Mellon University, 1998, Pp. viii+189. Available at http:/www.cs.emu.edu/~hwxi/DML/thesis.ps
• [29] Xi, H.: Dependently Typed Pattern Matching, Journal of Universal Computer Science, 9(8), 2003, 851-872.
• [30] Xi, H.: Applied Type System (extended abstract), post-workshop Proceedings of TYPES 2003, Springer-Verlag LNCS 3085, 2004.
• [31] Xi, H.: Applied Type System, 2005, Available at: http://www.cs.bu.edu/~hwxi/ATS
• [32] Xi, H., Chen, C., Chen, G.: Guarded Recursive Datatype Constructors, Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages, ACM press, New Orleans, LA, January 2003.
• [33] Xi, H., Pfenning, F.: Dependent Types in Practical Programming, Proceedings of 26th ACM SIGPLAN Symposium on Principles of Programming Languages, ACM press, San Antonio, Texas, January 1999.
• [34] Xi, H., Shi, R., Chen, C.: Typeful Closure Conversion, January 2005, Available at . http://www.cs.bu.edu/~hwxi/ATS/EXAMPLE/LF/cc.ats