Automatically Splitting a Two-Stage Lambda Calculus
详细信息 查看全文
- 刊名：Lecture Notes in Computer Science
- 出版年：2016
- 出版时间：2016
- 年：2016
- 卷：9632
- 期：1
- 页码：255-281
- 全文大小：1,451 KB
- 参考文献：1.Acar, U.A., Blelloch, G.E., Blume, M., Harper, R., Tangwongsan, K.: An experimental analysis of self-adjusting computation. ACM Trans. Prog. Lang. Sys. 32(1), 3:1–3:53 (2009)CrossRef
2.Bondorf, A., Danvy, O.: Automatic autoprojection of recursive equations with global variable and abstract data types. Sci. Comput. Program. 16(2), 151–195 (1991)CrossRef MATH
3.Consel, C.: New insights into partial evaluation: the schism experiment. In: Ganzinger, H. (ed.) ESOP ’88. Lecture Notes in Computer Science, vol. 300, pp. 236–246. Springer, Heidelberg (1988)CrossRef
4.Davies, R.: A temporal-logic approach to binding-time analysis. In: LICS, pp. 184–195 (1996)
5.Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555–604 (2001)MathSciNet CrossRef MATH
6.De Niel, A., Bevers, E., De Vlaminck, K.: Program bifurcation for a polymorphically typed functional language. SIGPLAN Not. 26(9), 142–153 (1991)CrossRef
7.Demers, A., Reps, T., Teitelbaum, T.: Incremental evaluation of attribute grammars with application to syntax-directed editors. In: Principles of Programming Languages, pp. 105–116 (1981)
8.Foley, T., Hanrahan, P.: Spark: modular, composable shaders for graphics hardware. ACM Trans. Graph. 30(4), 107:1–107:12 (2011)CrossRef
9.Futamura, Y.: Partial evaluation of computation process - an approach to a compiler-compiler. Syst. Comput. Controls 2(5), 45–50 (1971)
10.Gomard, C.K., Jones, N.D.: A partial evaluator for the untyped lambda-calculus. J. Funct. Program. 1(1), 21–69 (1991)MathSciNet CrossRef MATH
11.He, Y., Gu, Y., Fatahalian, K.: Extending the graphics pipeline with adaptive, multi-rate shading. ACM Trans. Graph. 33(4), 142:1–142:12 (2014)CrossRef
12.Hoare, C.A.R.: Algorithm 65: find. Commun. ACM 4(7), 321–322 (1961)CrossRef
13.Jones, N.D.: An introduction to partial evaluation. ACM Comput. Surv. 28(3), 480–503 (1996)CrossRef
14.Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall International Series in Computer Science. Prentice Hall, UPPER SADDLE RIVER (1993)MATH
15.Jørring, U., Scherlis, W.L.: Compilers and staging transformations. In: Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. POPL 1986, NY, USA, pp. 86–96. ACM, New York (1986)
16.Knoblock, T.B., Ruf, E.: Data specialization. In: Proceedings of the ACM SIGPLAN 1996 Conference on Programming Language Design and Implementation. PLDI 1996, NY, USA, pp. 215–225. ACM, New York (1996)
17.Mogensen, T.A.: Binding time analysis for polymorphically typed higher order languages. In: Díaz, J., Orejas, F. (eds.) TAPSOFT 1989. LNCS, vol. 352, pp. 298–312. Springer, Heidelberg (1989). Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages
18.Mogensen, T.A.: Separating binding times in language specifications. In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture. FPCA 1989, NY, USA, pp. 12–25. ACM, New York (1989)
19.Murphy VII, T., Crary, K., Harper, R.: Distributed control flow with classical modal logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 51–69. Springer, Heidelberg (2005)CrossRef
20.Nanevski, A., Pfenning, F.: Staged computation with names and necessity. J. Funct. Program. 15(5), 893–939 (2005)MathSciNet CrossRef MATH
21.Nielson, F., Nielson, H.R.: Two-level Functional Languages. Cambridge University Press, New York (1992)CrossRef MATH
22.Proudfoot, K., Mark, W.R., Tzvetkov, S., Hanrahan, P.: A real-time procedural shading system for programmable graphics hardware. In: Proceedings of the 28th Annual Conference on Computer Graphics and Interactive Techniques. SIGGRAPH 2001, pp. 159–170. ACM (2001)
23.Pugh, W., Teitelbaum, T.: Incremental computation via function caching. In: Principles of Programming Languages, pp. 315–328 (1989)
24.Ramalingam, G., Reps, T.: A categorized bibliography on incremental computation. In: Principles of Programming Languages, pp. 502–510 (1993)
25.Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM Annual Conference. ACM 1972, NY, USA, vol. 2, pp. 717–740. ACM, New York (1972)
26.Segal, M., Akeley, K.: The OpenGL Graphics System: A Specification (Version 4.0). The Khronos Group, Inc., Beaverton (2010)
27.Taha, W.: Multi-Stage Programming: Its Theory and Applications. Ph.D. thesis, Oregon Graduate Institute of Science and Technology(1999)
28.Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: Proceedings of the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation. PEPM 1997 (1997) - 作者单位：Nicolas Feltman (14)
Carlo Angiuli (14)
Umut A. Acar (14)
Kayvon Fatahalian (14)
14. Carnegie Mellon University, Pittsburgh, USA - 丛书名：Programming Languages and Systems
- ISBN：978-3-662-49498-1
- 刊物类别：Computer Science
- 刊物主题：Artificial Intelligence and Robotics
Computer Communication Networks
Software Engineering
Data Encryption
Database Management
Computation by Abstract Devices
Algorithm Analysis and Problem Complexity - 出版者：Springer Berlin / Heidelberg
- ISSN：1611-3349
文摘
Staged programming languages assign a stage to each program expression and evaluate each expression in its assigned stage. A common use of staged languages is to describe programs where inputs arrive at different times or rates. In this paper we present an algorithm for statically splitting these mixed-staged programs into two unstaged, but dependent, programs where the outputs of the first program can be efficiently reused across multiple invocations of the second. While previous algorithms for performing this transformation (also called pass separation and data specialization) were limited to operate on simpler, imperative languages, we define a splitting algorithm for an explicitly-two-stage, typed lambda calculus with a \(\bigcirc \) modality denoting computation at a later stage, and a \(\nabla \) modality noting purely first-stage code. Most notably, the algorithm splits mixed-stage recursive and higher-order functions. We prove the dynamic correctness of our splitting algorithm with respect to a partial-evaluation semantics, and mechanize this proof in Twelf. We also implement the algorithm in a prototype compiler, and demonstrate that the ability to split programs in a language featuring recursion and higher-order features enables non-trivial algorithmic transformations that improve code efficiency and also facilitates modular expression of staged programs.