Zoe Paraskevopoulou
Abstract
In this paper we present a novel simulation relation for proving correctness of program transformations that combines syntactic simulations and logical relations. In particular, we establish a new kind of simulation diagram that uses a small-step or big-step semantics in the source language and an untyped, step-indexed logical relation in the target language. Our technique provides a practical solution for proving semantics preservation for transformations that do not preserve reductions in the source language. This is common when transformations generate new binder names, and hence α-conversion must be explicitly accounted for, or when transformations introduce administrative redexes. Our technique does not require reductions in the source language to correspond directly to reductions in the target language. Instead, we enforce a weaker notion of semantic preorder, which suffices to show that semantics are preserved for both whole-program and separate compilation. Because our logical relation is transitive, we can transition between intermediate program states in a small-step fashion and hence the shape of the proof resembles that of a simple small-step simulation.
We use this technique to revisit the semantic correctness of a continuation-passing style (CPS) transformation and we demonstrate how it allows us to overcome well-known complications of this proof related to α-conversion and administrative reductions. In addition, by using a logical relation that is indexed by invariants that relate the resource consumption of two programs, we are able show that the transformation preserves diverging behaviors and that our CPS transformation asymptotically preserves the running time of the source program. Our results are formalized in the Coq proof assistant. Our continuation-passing style transformation is part of the CertiCoq compiler for Gallina, the specification language of Coq.
Supplemental Material
- Umut A. Acar, Amal Ahmed, and Matthias Blume. 2008. Imperative Self-Adjusting Computation. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’08). Association for Computing Machinery, New York, NY, USA. 309–322. isbn:9781595936899 https://doi.org/10.1145/1328438.1328476 Google Scholar
Digital Library
- Norman Adams, David Kranz, Richard Kelsey, Jonathan Rees, Paul Hudak, and James Philbin. 1986. ORBIT: An Optimizing Compiler for Scheme. In Proceedings of the 1986 SIGPLAN Symposium on Compiler Construction (SIGPLAN ’86). Association for Computing Machinery, New York, NY, USA. 219–233. isbn:0897911970 https://doi.org/10.1145/12276.13333 Google ScholarDigital Library
- Amal Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In Proceedings of the 15th European Conference on Programming Languages and Systems (ESOP’06). Springer-Verlag, Berlin, Heidelberg. 69–83. isbn:354033095X https://doi.org/10.1007/11693024_6 Google ScholarDigital Library
- Amal Ahmed and Matthias Blume. 2011. An Equivalence-Preserving CPS Translation via Multi-Language Semantics. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP ’11). Association for Computing Machinery, New York, NY, USA. 431–444. isbn:9781450308656 https://doi.org/10.1145/2034773.2034830 Google ScholarDigital Library
- Abhishek Anand, Andrew W. Appel, John Gregory Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Bélanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In CoqPL’17: The Third International Workshop on Coq for Programming Languages. 2 pages.Google Scholar
- Andrew W. Appel and Trevor Jim. 1997. Shrinking lambda expressions in linear time. Journal of Functional Programming, 7, 5 (1997), Sept., 515–540. issn:0956-7968 https://doi.org/10.1017/S0956796897002839 Google ScholarDigital Library
- Andrew W. Appel. 1992. Compiling with Continuations. Cambridge University Press, New York. Google ScholarDigital Library
- Andrew W. Appel and David McAllester. 2001. An Indexed Model of Recursive Types for Foundational Proof-Carrying Code. ACM Trans. Program. Lang. Syst., 23, 5 (2001), Sept., 657–683. issn:0164-0925 https://doi.org/10.1145/504709.504712 Google ScholarDigital Library
- Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. 2005. Mechanized Metatheory for the Masses: The PoplMark Challenge. In Theorem Proving in Higher Order Logics, Joe Hurd and Tom Melham (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 50–65. isbn:978-3-540-31820-0 https://doi.org/10.1007/11541868_4 Google ScholarDigital Library
- William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. 2017. Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible. Proc. ACM Program. Lang., 2, POPL (2017), Article 22, Dec., 33 pages. https://doi.org/10.1145/3158110 Google ScholarDigital Library
- Adam Chlipala. 2007. A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’07). Association for Computing Machinery, New York, NY, USA. 54–65. isbn:9781595936332 https://doi.org/10.1145/1250734.1250742 Google ScholarDigital Library
- Adam Chlipala. 2008. Parametric Higher-Order Abstract Syntax for Mechanized Semantics. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08). Association for Computing Machinery, New York, NY, USA. 143–156. isbn:9781595939197 https://doi.org/10.1145/1411204.1411226 Google ScholarDigital Library
- Oliver Danvy and Andrzex Filinski. 1992. Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science, 2, 4 (1992), 361–391. https://doi.org/10.1017/S0960129500001535 Google ScholarCross Ref
- Olivier Danvy and Lasse R. Nielsen. 2003. A first-order one-pass CPS transformation. Theoretical Computer Science, 308, 1 (2003), 239–257. issn:0304-3975 https://doi.org/10.1016/S0304-3975(02)00733-8 Google ScholarDigital Library
- Zaynah Dargaye and Xavier Leroy. 2007. Mechanized Verification of CPS Transformations. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’07). Springer-Verlag, Berlin, Heidelberg. 211–225. isbn:3540755586 Google ScholarDigital Library
- Timothy G. Griffin. 1989. A Formulae-as-Type Notion of Control. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’90). Association for Computing Machinery, New York, NY, USA. 47–58. isbn:0897913434 https://doi.org/10.1145/96709.96714 Google ScholarDigital Library
- Robert Harper and Mark Lillibridge. 1993. Explicit Polymorphism and CPS Conversion. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’93). Association for Computing Machinery, New York, NY, USA. 206–219. isbn:0897915607 https://doi.org/10.1145/158511.158630 Google ScholarDigital Library
- Andrew Kennedy. 2007. Compiling with Continuations, Continued. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP ’07). ACM, New York, NY, USA. 177–190. isbn:978-1-59593-815-2 https://doi.org/10.1145/1291151.1291179 Google ScholarDigital Library
- Xavier Leroy. 2009. A Formally Verified Compiler Back-End. J. Autom. Reason., 43, 4 (2009), Dec., 363–446. issn:0168-7433 https://doi.org/10.1007/s10817-009-9155-4 Google ScholarDigital Library
- Yasuhiko Minamide. 1999. Space-Profiling Semantics of the Call-by-Value Lambda Calculus and the CPS Transformation. Electr. Notes Theor. Comput. Sci., 26 (1999), 105–120. https://doi.org/10.1016/S1571-0661(05)80286-5 Google ScholarCross Ref
- Yasuhiko Minamide and Koji Okuma. 2003. Verifying CPS Transformations in Isabelle/HOL. In Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN ’03). Association for Computing Machinery, New York, NY, USA. 1–8. isbn:1581138008 https://doi.org/10.1145/976571.976576 Google ScholarDigital Library
- Greg Morrisett, David Walker, Karl Crary, and Neal Glew. 1999. From System F to Typed Assembly Language. ACM Trans. Program. Lang. Syst., 21, 3 (1999), May, 527–568. issn:0164-0925 https://doi.org/10.1145/319301.319345 Google ScholarDigital Library
- Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In Programming Languages and Systems, Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 589–615. isbn:978-3-662-49498-1 https://doi.org/10.1007/978-3-662-49498-1_23 Google ScholarDigital Library
- Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan. 2017. Verifying Efficient Function Calls in CakeML. Proc. ACM Program. Lang., 1, ICFP (2017), Article 18, Aug., 27 pages. issn:2475-1421 https://doi.org/10.1145/3110262 Google ScholarDigital Library
- Zoe Paraskevopoulou and Andrew W. Appel. 2019. Closure Conversion is Safe for Space. Proc. ACM Program. Lang., 3, ICFP (2019), Article 83, July, 29 pages. https://doi.org/10.1145/3341687 Google ScholarDigital Library
- Zoe Paraskevopoulou and Anvay Grover. 2021. [OOPSLA 2021 Artifact] Compiling With Continuations, Correctly. https://doi.org/10.5281/zenodo.5504155 Google ScholarDigital Library
- Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel. 2021. Compositional Optimizations for CertiCoq. Proc. ACM Program. Lang., 3, ICFP (2021), Article 86, July, 30 pages. https://doi.org/10.1145/3341687 Google ScholarDigital Library
- G.D. Plotkin. 1975. Call-by-name, call-by-value and the λ -calculus. Theoretical Computer Science, 1, 2 (1975), 125 – 159. issn:0304-3975 https://doi.org/10.1016/0304-3975(75)90017-1 Google ScholarCross Ref
- François Pottier. 2017. Revisiting the CPS Transformation and its Implementation. Unpublished.Google Scholar
- Amr Sabry and Matthias Felleisen. 1992. Reasoning about Programs in Continuation-Passing Style.. SIGPLAN Lisp Pointers, V, 1 (1992), Jan., 288–298. issn:1045-3563 https://doi.org/10.1145/141478.141563 Google ScholarDigital Library
- Olivier Savary Bélanger and Andrew W. Appel. 2017. Shrink Fast Correctly!. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming (PPDP ’17). Association for Computing Machinery, New York, NY, USA. 49–60. isbn:9781450352918 https://doi.org/10.1145/3131851.3131859 Google ScholarDigital Library
- Guy L. Steele. 1978. Rabbit: A Compiler for Scheme. USA. Google ScholarDigital Library
- Ye Henry Tian. 2006. Mechanically Verifying Correctness of CPS Compilation. In Proceedings of the Twelfth Computing: The Australasian Theory Symposium - Volume 51 (CATS ’06). Australian Computer Society, Inc., AUS. 41–51. isbn:1920682333 Google ScholarDigital Library
- Urara Yamada and Kenichi Asai. 2018. Certifying CPS Transformation of Let-Polymorphic Calculus Using PHOAS. In Programming Languages and Systems, Sukyoung Ryu (Ed.). Springer International Publishing, Cham. 375–393. isbn:978-3-030-02768-1 https://doi.org/10.1007/978-3-030-02768-1_20 Google ScholarCross Ref
Index Terms
- Compiling with continuations, correctly
Recommendations
Compositional semantics for composable continuations: from abortive to delimited control
ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programmingParigot's λμ-calculus, a system for computational reasoning about classical proofs, serves as a foundation for control operations embodied by operators like Scheme's callcc. We demonstrate that the call-by-value theory of the λμ-calculus contains a ...
Coinductive big-step operational semantics
Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We ...
Closure conversion is safe for space
We formally prove that closure conversion with flat environments for CPS lambda calculus is correct (preserves semantics) and safe for time and space, meaning that produced code preserves the time and space required for the execution of the source ...
Comments