Abstract
We settle three basic questions that naturally arise when verifying multi-stage functional programs. Firstly, does adding staging to a language compromise any equalities that hold in the base language? Unfortunately it does, and more care is needed to reason about terms with free variables. Secondly, staging annotations, as the name “annotations” suggests, are often thought to be orthogonal to the behavior of a program, but when is this formally guaranteed to be true? We give termination conditions that characterize when this guarantee holds. Finally, do multi-stage languages satisfy useful, standard extensional facts—for example, that functions agreeing on all arguments are equivalent? We provide a sound and complete notion of applicative bisimulation, which establishes such facts or, in principle, any valid program equivalence. These results greatly improve our understanding of staging, and allow us to prove the correctness of quite complicated multi-stage programs.
Supported in part by NSF grant CCF-0747431; NSF Award # 0747431, “Multi-stage programming for object-oriented languages”; and NSF Award # 0720857, “Building physically safe embedded systems”.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S.: The Lazy Lambda Calculus, pp. 65–116. Addison-Wesley, Boston (1990)
Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and The Foundations of Mathematics. North-Holland (1984)
Berger, M., Tratt, L.: Program Logics for Homogeneous Meta-programming. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 64–81. Springer, Heidelberg (2010)
Brady, E., Hammond, K.: A verified staged interpreter is a verified compiler. In: 5th International Conference on Generative Programming and Component Engineering, pp. 111–120. ACM (2006)
Carette, J., Kiselyov, O.: Multi-stage Programming with Functors and Monads: Eliminating Abstraction Overhead from Generic Code. In: Glück, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol. 3676, pp. 256–274. Springer, Heidelberg (2005)
Carette, J., Kiselyov, O., Shan, C.-C.: Finally Tagless, Partially Evaluated: Tagless Staged Interpreters for Simpler Typed Languages. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 222–238. Springer, Heidelberg (2007)
Choi, W., Aktemur, B., Yi, K., Tatsuta, M.: Static analysis of multi-staged programs via unstaging translation. In: 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 81–92. ACM, New York (2011)
Cohen, A., Donadio, S., Garzaran, M.J., Herrmann, C., Kiselyov, O., Padua, D.: In search of a program generator to implement generic transformations for high-performance computing. Sci. Comput. Program. 62(1), 25–46 (2006)
Dybvig, R.K.: Writing hygienic macros in scheme with syntax-case. Tech. Rep. TR356, Indiana University Computer Science Department (1992)
Gordon, A.D.: Bisimilarity as a theory of functional programming. Theoretical Computer Science 228(1-2), 5–47 (1999)
Heizmann, M., Jones, N., Podelski, A.: Size-Change Termination and Transition Invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 22–50. Springer, Heidelberg (2010)
Herrmann, C.A., Langhammer, T.: Combining partial evaluation and staged interpretation in the implementation of domain-specific languages. Sci. Comput. Program. 62(1), 47–65 (2006)
Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103–112 (1996)
Inoue, J., Taha, W.: Reasoning about multi-stage programs. Tech. rep., Rice University Computer Science Department (October 2011)
Intrigila, B., Statman, R.: The Omega Rule is \({\bf{\Pi}^{1}_{1}}\)-Complete in the λβ-Calculus. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 178–193. Springer, Heidelberg (2007)
Kameyama, Y., Kiselyov, O., Shan, C.-C.: Shifting the stage: Staging with delimited control. In: 2009 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 111–120. ACM, New York (2009)
Kim, I.S., Yi, K., Calcagno, C.: A polymorphic modal type system for LISP-like multi-staged languages. In: 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 257–268. ACM, New York (2006)
Kiselyov, O., Swadi, K.N., Taha, W.: A methodology for generating verified combinatorial circuits. In: Proc. of EMSOFT, pp. 249–258. ACM (2004)
Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: 2006 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, pp. 141–152. ACM, New York (2006)
Muller, R.: M-LISP: A representation-independent dialect of LISP with reduction semantics. ACM Trans. Program. Lang. Syst., 589–616 (1992)
Plotkin, G.D.: The λ-calculus is ω-incomplete. J. Symb. Logic, 313–317 (June 1974)
Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74 (2002)
Rompf, T., Odersky, M.: Lightweight modular staging: A pragmatic approach to runtime code generation and compiled DSLs. In: 9th International Conference on Generative Programming and Component Engineering (2010)
Sands, D.: Improvement Theory and its Applications, pp. 275–306. Cambridge University Press, New York (1998)
Swadi, K., Taha, W., Kiselyov, O., Pašalić, E.: A monadic approach for avoiding code duplication when staging memoized functions. In: 2006 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, pp. 160–169. ACM, New York (2006)
Taha, W.: Multistage Programming: Its Theory and Applications. Ph.D. thesis, Oregon Graduate Institute (1999)
Taha, W., Nielsen, M.F.: Environment classifiers. In: 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 26–37. ACM, New York (2003)
Tsukada, T., Igarashi, A.: A Logical Foundation for Environment Classifiers. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 341–355. Springer, Heidelberg (2009)
Westbrook, E., Ricken, M., Inoue, J., Yao, Y., Abdelatif, T., Taha, W.: Mint: Java multi-stage programming using weak separability. In: 2010 Conference on Programming Language Design and Implementation (2010)
Yang, Z.: Reasoning about code-generation in two-level languages. Tech. Rep. RS-00-46, BRICS (2000)
Yuse, Y., Igarashi, A.: A modal type system for multi-level generating extensions with persistent code. In: 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 201–212. ACM, New York (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Inoue, J., Taha, W. (2012). Reasoning about Multi-stage Programs. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)