Abstract
Transformation to continuation-passing style (CPS) is often performed by optimizing compilers for functional programming languages. As part of the development and proof of correctness of a compiler for the mini-ML functional language, we have mechanically verified the correctness of two CPS transformations for a call-by-value λ-calculus with n-ary functions, recursive functions, data types and pattern-matching. The transformations generalize Plotkin’s original call-by-value transformation and Danvy and Nielsen’s optimized transformation, respectively. We used the Coq proof assistant to formalize the transformations and conduct and check the proofs. Originalities of this work include the use of big-step operational semantics to avoid difficulties with administrative redexes, and of two-sorted de Bruijn indices to avoid difficulties with α-conversion.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. Journal of Functional Programming 1(4), 375–416 (1991)
Appel, A.W.: Compiling with continuations. Cambridge University Press, Cambridge (1992)
Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. In: EATCS Texts in Theoretical Computer Science, Springer, Heidelberg (2004)
Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 460–475. Springer, Heidelberg (2006)
Chlipala, A.: A certified type-preserving compiler from lambda calculus to assembly language. In: Programming Language Design and Implementation 2007, pp. 54–65. ACM Press, New York (2007)
Coq development team. The Coq proof assistant. Software and documentation (1989–2007), available at http://coq.inria.fr/
Danvy, O., Nielsen, L.R.: A first-order one-pass CPS transformation. Theoretical Computer Science 308(1-3), 239–257 (2003)
Danvy, O., Nielsen, L.R.: CPS transformation of beta-redexes. Information Processing Letters 94(5), 217–224 (2005)
Dargaye, Z.: Décurryfication certifiée. In: Journées Francophones des Langages Applicatifs (JFLA 2007), INRIA (2007)
de Bruijn, N.G.: Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math. 34(5), 381–392 (1972)
Flanagan, C., Sabry, A., Duba, B., Felleisen, M.: The essence of compiling with continuations. In: Programming Language Design and Implementation 1993, pp. 237–247. ACM Press, New York (1993)
Kennedy, A.: Compiling with continuations, continued. In: International Conference on Functional Programming, ACM Press, New York (2007)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Transactions on Programming Languages and Systems 28(4), 619–695 (2006)
Kranz, D., Adams, N., Kelsey, R., Rees, J., Hudak, P., Philbin, J.: ORBIT: an optimizing compiler for Scheme. In: SIGPLAN 1986. symposium on Compiler Construction, pp. 219–233. ACM Press, New York (1986)
Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In: SEFM 2005. Int. Conf. on Software Engineering and Formal Methods, pp. 2–11. IEEE Computer Society Press, Los Alamitos (2005)
Leroy, X.: Coinductive big-step operational semantics. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 54–68. Springer, Heidelberg (2006)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd symposium Principles of Programming Languages, pp. 42–54. ACM Press, New York (2006)
Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200–219. Springer, Heidelberg (2003)
Minamide, Y., Okuma, K.: Verifying CPS transformations in Isabelle/HOL. In: MERLIN 2003. Proc. workshop on Mechanized reasoning about languages with variable binding, pp. 1–8. ACM Press, New York (2003)
Moore, J.S.: Piton: a mechanically verified assembly-language. Kluwer Academic Publishers, Dordrecht (1996)
Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science 1(2), 125–159 (1975)
Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Transactions on Programming Languages and Systems 19(6), 916–941 (1997)
Tian, Y.H.: Mechanically verifying correctness of CPS compilation. In: CATS 2006. Proceedings of the 12th Computing: The Australasian Theory Symposium, pp. 41–51. Australian Computer Society (2006)
Urban, C.: Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning (to appear, 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dargaye, Z., Leroy, X. (2007). Mechanized Verification of CPS Transformations. In: Dershowitz, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2007. Lecture Notes in Computer Science(), vol 4790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75560-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-75560-9_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75558-6
Online ISBN: 978-3-540-75560-9
eBook Packages: Computer ScienceComputer Science (R0)