A modal analysis of staged computation

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A modal analysis of staged computation

Full text

Pdf (1.21 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

St. Petersburg Beach, Florida, United States

Pages: 258 - 270

Year of Publication: 1996

ISBN:0-89791-769-3

Authors

Rowan Davies	Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA
Frank Pfenning	Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 20, Citation Count: 37

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/237721.237788 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	BdP92	Gavin Bierman and Valeria de Paiva. Intuitionistic necessity revisited. In Proceedings of the Logic at Work Conference, Amsterdam, Holiand, December 1992.
	BW93	Lars Birkedal and Morton Welinder. Partial evaluation of Standard ML. Master's thesis, University of Copenhagen, Department of Computer Science, 1993. Available as Technical Report DIKU-report 93/22.
	CDDK86	Dominique Clément , Thierry Despeyroux , Gilles Kahn , Joëlle Despeyroux, A simple applicative language: mini-ML, Proceedings of the 1986 ACM conference on LISP and functional programming, p.13-27, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319847]
	Dav95	Rowan Davies. A temporal-logic approach to binding-time analysis. Research Series RS-95- 51, BRtCS, Department of Computer Science, University of Aarhus, October 1995.
	FP91	Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
	GJ91	Carsten Oomard and Neil Jones. A partial evaluator for ehe untyped tambda-calculus. Journal of Functzonal Programming, 1(1):21#69, January 1991.
	GJ95	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
	Hat95	John Hatcliff, Mechanically Verifying the Correctness of an Offline Partial Evaluator, Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs, p.279-298, September 20-22, 1995
	Hen91	Fritz Henglein, Efficient type inference for higher-order binding-time analysis, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.448-472, June 1991, Cambridge, Massachusetts, United States
	JGS93	Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
	Jon91	Neil D. Jones, Efficient Algebraic Operations on Programs, Proceedings of the Second International Conference on Methodology and Software Technology: Algebraic Methodology and Software Technology, p.393-420, May 22-25, 1991
	JS86	Ulrik Jørring , William L. Scherlis, Compilers and staging transformations, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.86-96, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512652]
	KEH93	David Keppel, Susan J. Eggers, and Robert R. Henry. A case for runtime code generation. Technical Report TR 93-11-02, Department of Computer Science and Engineering, University of Washington, November 1993.
	Kri63	Saul A. Kripke. Semantic analysis of modal logic. I: Normal propositional calculi. Zeitschrift fiir Mathematische Logik und Grundlagen der Mathemat#k, 9:67-96, 1963.
	LL94	Mark Leone , Peter Lee, Deferred Compilation: The Automation of Run-Time Code Generation, Carnegie Mellon University, Pittsburgh, PA, 1993
	MM94	Simone Martini and Andrea Masini. A computational interpretation of modal proofs. In H. Wansing, editor, Proof theory of Modal Log- #cs. Kluwer, 1994. Workshop proceedings.
	Mog89	E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
	NN92	Flemming Nielson , Hanne Riis Nielson, Two-level functional languages, Cambridge University Press, New York, NY, 1992
	Pal93	Jens Palsberg. Correctness of binding time analysis. Journal of Functional Programming, 3(3):347-363, July 1993.
	Pfe91	Frank Pfenning, Logic programming in the LF logical framework, Logical frameworks, Cambridge University Press, New York, NY, 1991
	PW95	Frank Pfenning and Hao-Chi Wong. On a modal A-calculus for $4. In S. Brookes and M. Main, editors, Proceedings of the Eleventh Conference on Mathematical Foundations of Programming Semat#cs, New Orleans, Louisiana, March 1995.
	Smi84	Brian Cantwell Smith, Reflection and semantics in LISP, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.23-35, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800513]
	SN95	Tim Sheard and Neal Nelson. Type safe abstractions using program generators. Technical Report OGI-TR-95-013, Oregon Graduate Institute of Science and Technology, Department of Computer Science, t995.

CITED BY 37

	Peter Lee , Mark Leone, Optimizing ML with run-time code generation, ACM SIGPLAN Notices, v.31 n.5, p.137-148, May 1996
	Philip Wickline , Peter Lee , Frank Pfenning , Rowan Davies, Modal types as staging specifications for run-time code generation, ACM Computing Surveys (CSUR), v.30 n.3es, Sept. 1998
	Rowan Davies , Frank Pfenning, A modal analysis of staged computation, Journal of the ACM (JACM), v.48 n.3, p.555-604, May 2001
	Zhe Yang, Encoding types in ML-like languages, ACM SIGPLAN Notices, v.34 n.1, p.289-300, Jan. 1999
	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
	Walid Taha , Tim Sheard, Multi-stage programming (poster), ACM SIGPLAN Notices, v.32 n.8, p.321, Aug. 1997
	Frank Pfenning, On the logical foundations of staged computation (invited talk), ACM SIGPLAN Notices, v.34 n.11, p.33, Nov. 1999
	Mark Leone , Peter Lee, Dynamic specialization in the Fabius system, ACM Computing Surveys (CSUR), v.30 n.3es, Sept. 1998
	Philip Wickline , Peter Lee , Frank Pfenning, Run-time code generation and modal-ML, ACM SIGPLAN Notices, v.33 n.5, p.224-235, May 1998
	Flemming Nielson , Hanne Riis Nielson, Prescriptive frameworks for multi-level lambda-calculi, ACM SIGPLAN Notices, v.32 n.12, p.193-202, Dec. 1997
	Carsten Schurmann , Joelle Despeyroux , Frank Pfenning, Primitive recursion for higher-order abstract syntax, Theoretical Computer Science, v.266 n.1-2, p.1-57, 09/06/2001
	Walid Taha , Tim Sheard, Multi-stage programming with explicit annotations, ACM SIGPLAN Notices, v.32 n.12, p.203-217, Dec. 1997
	Steven E. Ganz , Amr Sabry , Walid Taha, Macros as multi-stage computations: type-safe, generative, binding macros in MacroML, ACM SIGPLAN Notices, v.36 n.10, October 2001
	Olivier Danvy, Type-directed partial evaluation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.242-257, January 21-24, 1996, St. Petersburg Beach, Florida, United States
	Walid Taha , Michael Florentin Nielsen, Environment classifiers, ACM SIGPLAN Notices, v.38 n.1, p.26-37, January 2003
	Matthew Flatt, Composable and compilable macros:: you want it when?, ACM SIGPLAN Notices, v.37 n.9, p.72-83, September 2002
	Aleksandar Nanevski, From dynamic binding to state via modal possibility, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.207-218, August 27-29, 2003, Uppsala, Sweden
	Walid Taha, A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trival (extended abstract), ACM SIGPLAN Notices, v.34 n.11, p.34-43, Nov. 1999
	Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States
	Peter Lee , Mark Leone, Optimizing ML with run-time code generation, ACM SIGPLAN Notices, v.39 n.4, April 2004
	Peter Lee , Mark Leone, Optimizing ML with run-time code generation, ACM SIGPLAN Notices, v.39 n.4, April 2004
	Zhe Yang, Encoding types in ML-like languages, Theoretical Computer Science, v.315 n.1, p.151-190, 5 May 2004
	Emir PašaliΕ , Walid Taha , Tim Sheard, Tagless staged interpreters for typed languages, ACM SIGPLAN Notices, v.37 n.9, p.218-229, September 2002
	Serenella Cerrito , Delia Kesner, Pattern matching as cut elimination, Theoretical Computer Science, v.323 n.1-3, p.71-127, 14 September 2004
	Aleksandar Nanevski, Meta-programming with names and necessity, ACM SIGPLAN Notices, v.37 n.9, p.206-217, September 2002
	Cristiano Calcagno , Walid Taha , Liwen Huang , Xavier Leroy, Implementing multi-stage languages using ASTs, Gensym, and reflection, Proceedings of the second international conference on Generative programming and component engineering, p.57-76, September 22-25, 2003, Erfurt, Germany
	Ik-Soon Kim , Kwangkeun Yi , Cristiano Calcagno, A polymorphic modal type system for lisp-like multi-staged languages, ACM SIGPLAN Notices, v.41 n.1, p.257-268, January 2006
	Matt Fairtlough , Michael Mendler , Eugenio Moggi, Special issue: Modalities in type theory, Mathematical Structures in Computer Science, v.11 n.4, p.507-509, August 2001
	Frank Pfenning , Rowan Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, v.11 n.4, p.511-540, August 2001
	Joëlle Despeyroux , Pierre Leleu, Recursion over objects of functional type, Mathematical Structures in Computer Science, v.11 n.4, p.555-572, August 2001
	Andrew D. Eisenberg , Gregor Kiczales, Expressive programs through presentation extension, Proceedings of the 6th international conference on Aspect-oriented software development, March 12-16, 2007, Vancouver, British Columbia, Canada
	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
	John Hatcliff , Olivier Danvy, A computational formalization for partial evaluation, Mathematical Structures in Computer Science, v.7 n.5, p.507-541, October 1997
	Frederick Smith , Dan Grossman , Greg Morrisett , Luke Hornof , Trevor Jim, Compiling for template-based run-time code generation, Journal of Functional Programming, v.13 n.3, p.677-708, May 2003
	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
	Stefan Monnier , Zhong Shao, Inlining as staged computation, Journal of Functional Programming, v.13 n.3, p.647-676, May 2003
	Roly Perera, Programming Languages For Interactive Computing, Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.3, p.35-52, May, 2008