Rowan Davies
Skip Abstract Section
Abstract
We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of typed λ-calculi and functional languages. We directly demonstrate the sense in which our λe→□-calculus captures staging, and also give a conservative embeddng of Nielson and Nielson's two-level functional language in our functional language Mini-ML□, thus proving that binding-time correctness is equivalent to modal correctness on this fragment. In addition, Mini-ML□ can also express immediate evaluation and sharing of code across multiple stages, thus supporting run-time code generation as well as partial evaluation.
- ANDREOLI, J.-M. 1992. Logic programming with focusing proofs in linear logic. J. Logic Comput. 2, 3, 197-347.]]Google Scholar
- BENTON,P.N.,BIERMAN,G.M.,AND DE PAIVA, V. C. V. 1998. Computational types from a logical perspective. J. Funct. Prog. 8, 2 (Mar.), 177-193.]] Google Scholar
- BIERMAN, G., AND DE PAIVA, V. 1996. Intuitionistic necessity revisited. Tech. Rep. CSRP-96-10 (June). School of Computer Science, Univ. Birmingham, Birmingham, Al.]]Google Scholar
- BIRKEDAL, L., AND WELINDER, M. 1993. Partial evaluation of Standard ML. Master's thesis. Dept. Comput. Sci., Univ. Copenhagen, Copenhagen, Denmark. Available as Tech. Rep. DIKU-report 93/22.]]Google Scholar
- BORGHUIS, T. 1994. Coming to terms with modal logic: On the interpretation of modalities in typed II-calculus. Ph.D. dissertation. Eindhoven University of Technology, Eindhoven, The Netherlands.]]Google Scholar
- CHELLAS, B. 1980. Modal Logic: An Introduction. Cambridge University Press, Cambridge, Mass., and New York.]]Google Scholar
- CLEMENT, D., DESPEYROUX, J., DESPEYROUX, T., AND KAHN, G. 1986. A simple applicative language: Mini-ML. In Proceedings of the 1986 Conference on LISP and Functional Programming (LFP'86) (Cambridge, Mass., Aug.). ACM, New York, pp. 13-27.]] Google Scholar
- CONSEL, C., AND NOEL, F. 1996. A general approach for run-time specialization and its application to C. In Proceedings of the 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'96) (St. Petersburg Beach, Fla., Jan. 21-24). ACM, New York, pp. 145-156.]] Google Scholar
- DAVIES, R. 1996. A temporal-logic approach to binding-time analysis. In Proceedings of the 11th Annual Symposium on Logic in Computer Science (LICS'96) E. Clarke Ed., (July). IEEE Computer Society Press, Los Alamitos, Calif., pp. 184-195.]] Google Scholar
- DAVIES, R., AND PFENNING, F. 1996. A modal analysis of staged computation. In Proceedings of the 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'96) (St. Petersburg Beach, Fla., Jan. 21-24). ACM, New York, pp. 258-270.]] Google Scholar
- DESPEYROUX, J., PFENNING, F., AND SCHURMANN, C. 1997. Primitive recursion for higher-order abstract syntax. In Proceedings of the 3rd International Conference on Typed Lambda Calculus and Applications (TLCA'97) (Nancy, France, Apr.)., R. Hindley Ed., Lecture Notes in Computer Science, vol. 1210. Springer-Verlag, New York, pp. 147-163. An extended version is available as Technical Report CMU-CS-96-172, Carnegie Mellon Univ., Pittsburgh, Pa.]] Google Scholar
- ENGLER,D.R.,HSIEH,W.C.,AND KAASHOEK, M. F. 1996. C: A language for high-level, efficient, and machine-independent dynamic code generation. In Proceedings of the 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'96) (St. Petersburg Beach, Fla., Jan. 21-24). ACM, New York, pp. 131-144.]] Google Scholar
- FAIRTLOUGH, M., AND MENDLER, M. 1997. Propositional lax logic. Inf. Comput. 137, 1 (Aug.), 1-33.]] Google Scholar
- GIRARD, J.-Y. 1993. On the unity of logic. Ann. Pure Appl. Logic 59, 201-217.]]Google Scholar
- GLUCK, R., AND JORGENSEN, J. 1995. Efficient multi-level generating extensions for program specialization. In Proceedings of the 7th International Symposium on Programming Languages, Implementations, Logics and Programs (PLILP'95) (Sept.). S. Swierstra and M. Hermenegildo, eds. Lecture Notes in Computer Science, vol. 982. Springer-Verlag, New York, pp. 259-278.]] Google Scholar
- GOMARD, C., AND JONES, N. 1991. A partial evaluator for the untyped lambda-calculus. J. Funct. Prog. 1, 1 (Jan.), 21- 69.]]Google Scholar
- GOUBAULT-LARRECQ, J. 1996. On computational interpretations of the modal logic S4, parts I-III. Tech. Rep. 1996-33,34,35. Institut fur Logik, Komplexitat und Deduktionssysteme, Universitat Karlsruhe, Karlsruhe, Germany.]]Google Scholar
- GOUBAULT-LARRECQ, J. 1997. On computational interpretations of the modal logic S4-IIIb. confluence, termination of the IIevQH -calculus. Tech. Rep. 3164 (May). INRIA, France.]]Google Scholar
- HATCLIFF, J. 1995. Mechanically verifying the correctness of an offline partial evaluator. In Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs (PLILP'95) (Utrecht, The Netherlands, Sept.). M. Hermenegildo and S. Swierstra, eds. Lecture Notes in Computer Science, vol. 982. Springer-Verlag, New York, pp. 279-298.]] Google Scholar
- HOFMANN, M. 1998. A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion. In Computer Science Logic (CSL'97): Annual Conference of the EACSL (Selected Papers) (Aarhus, Denmark, Aug.). M. Nielsen and W. Thomas, eds. Lecture Notes in Computer Science, vol. 1414. Springer-Verlag, New York, pp. 275-294.]] Google Scholar
- HOFMANN, M. 2000. Programming languages capturing complexity classes. ACM SIGACT News 31, 1 (Mar.), 31- 42.]] Google Scholar
- JONES, N. D. 1992. Efficient algebraic operations on programs. In Algebraic Methodology and Software Technology (AMAST'91): Proceedings of the Second International Conference. M. Nivat, C. Rattray, T. Rus, and G. Scollo, eds. Springer, London, England, pp. 393- 420. (A version appears as a chapter in Jones et al. {1993}.)]] Google Scholar
- JONES,N.D.,GOMARD, C., AND SESTOFT, P. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, International Series in Computer Science, Englewood Cliffs, N.J.]] Google Scholar
- JORRING, U., AND SCHERLIS, W. L. 1986. Compilers and staging transformations. In Conference Record of the 13th Annual ACM Symposium on Principles of Programming Languages (POPL'86) (St. Petersburg Beach, Fla., Jan.). ACM, New York, pp. 86-96.]] Google Scholar
- KEPPEL, D., EGGERS,S.J.,AND HENRY, R. R. 1993. A case for runtime code generation. Tech. Rep. TR 93-11-02 (Nov.). Dept. Comput. Sci. Eng., Univ. Washington, Seattle, Wash.]]Google Scholar
- KOBAYASHI, S. 1997. Monad as modality. Theoret. Comput. Sci. 175,29-74.]] Google Scholar
- KRIPKE, S. A. 1963. Semantic analysis of modal logic. I: Normal propositional calculi. Zeitsc. Math. Logik Grund. Math. 9,67-96.]]Google Scholar
- LEE, P., AND LEONE, M. 1996. Optimizing ML with run-time code generation. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'96) (Philadelphia, Pa., May 21-24). ACM, New York, pp. 137-148.]] Google Scholar
- LEONE, M., AND LEE, P. 1994. Lightweight run-time code generation. In Proceedings of the Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM'94) (Orlando, Fla., June). ACM, New York.]]Google Scholar
- MARTIN-LOF, P. 1996. On the meanings of the logical constants and the justifications of the logical laws. Nordic J. Philos. Logic 1,1,11- 60.]]Google Scholar
- MARTINI, S., AND MASINI, A. 1996. A computational interpretation of modal proofs. In Proof Theory of Modal Logics, H. Wansing, ed. Kluwer, Dordrecht, The Netherlands, pp. 213-241.]]Google Scholar
- MOGGI, E. 1989. Computational lambda calculus and monads. In Proceedings of the 4th Symposium on Logic in Computer Science (LICS'89) (Asilomar, Calif., June). IEEE Computer Society Press, Los Alamitos, Calif., pp. 14-23.]] Google Scholar
- MOGGI, E. 1991. Notions of computation and monads. Inf. Comput. 93,1,55-92.]] Google Scholar
- MOGGI, E., TAHA, W., BENAISSA, Z.-E.-A., AND SHEARD, T. 1999. An idealized MetaML: Simpler, and more expressive. In Proceedings of the European Symposium on Programming (Amsterdam, The Netherlands, Mar.), Lecture Notes in Computer Science, vol. 1576. Springer-Verlag, New York, pp. 193-207.]] Google Scholar
- NIELSON, F., AND NIELSON, H. R. 1992. Two-Level Functional Languages. Cambridge University Press, Cambridge, Mass.]] Google Scholar
- PALSBERG, J. 1993. Correctness of binding time analysis. J. Funct. Prog. 3, 3 (July), 347-363.]]Google Scholar
- PFENNING, F. 1991. Logic programming in the LF logical framework. In Logical Frameworks.G. Huet and G. Plotkin, eds., Cambridge University Press, Cambridge, Mass., pp. 149-181.]] Google Scholar
- PFENNING, F., AND DAVIES, R. 2001. A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. To appear.]] Google Scholar
- PFENNING, F., AND WONG, H.-C. 1995. On a modal II-calculus for S4. In Proceedings of the 11th Conference on Mathematical Foundations of Programming Semantics (MFPS'95) (New Orleans, La., Mar.). S. Brookes and M. Main, eds. Available as Electronic Notes in Theoretical Computer Science, Vol. 1. Elsevier, Amsterdam, The Netherlands.]]Google Scholar
- PRAWITZ, D. 1965. Natural Deduction. Almquist & Wiksell, Stockholm, Sweden.]]Google Scholar
- SMITH, B. C. 1984. Reflection and semantics in LISP.InProceedings of the 11th Annual ACM Symposium on Principles of Programming Languages (POPL'84) (Salt Lake City, Ut., Jan.). ACM, New York, pp. 23-35.]] Google Scholar
- TAHA, W., BENAISSA, Z.-E.-A., AND SHEARD, T. 1998. Multi-stage programming: Axiomatization and type safety. In Proceedings of the International Colloquium on Automata, Languages, and Programming (ICALP'98) (July), Lecture Notes in Computer Science, vol. 1443. Springer-Verlag, New York, pp. 918-929.]] Google Scholar
- TAHA, W., AND SHEARD, T. 1997. Multi-stage programming with explicit annotations. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'97) (Amsterdam, The Netherlands, June 12-13). ACM, New York, pp. 203-217.]] Google Scholar
- WADLER, P. 1993. A taste of linear logic. In Mathematical Foundations of Computing Science (MFCS'93) (Gdansk, Poland, Aug.). Lecture Notes in Computer Science, vol. 711. Springer- Verlag, New York, pp. 185-210.]] Google Scholar
- WICKLINE, P., LEE, P., AND PFENNING, F. 1998a. Modal types as staging specifications for runtime code generation. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'98) (Montreal, Ont. Canada, June 17-19). K. D. Cooper, Ed. ACM, New York, pp. 224-235.]] Google Scholar
- WICKLINE, P., LEE, P., PFENNING, F., AND DAVIES, R. 1998b. Modal types as staging specifications for run-time code generation. ACM Comput. Surv. 30, (Sept.), 3es.]] Google Scholar
Index Terms
- A modal analysis of staged computation
Recommendations
A Temporal Logic Approach to Binding-Time Analysis
This article demonstrates that there is a fundamental relationship between temporal logic and languages that involve multiple stages, such as those used to analyze binding times in the context of partial evaluation. This relationship is based on an ...
Classical Natural Deduction for S4 Modal Logic
AbstractThis paper proposes a natural deduction system CNDS4 for classical S4 modal logic with necessity and possibility modalities. This new system is an extension of Parigot’s Classical Natural Deduction with dualcontext to formulate S4 modal logic. The ...
A modal analysis of staged computation
POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of functional languages. Our main technical result is a conservative embedding of ...
Comments