Abstract
Establishing that two programs are contextually equivalent is hard, yet essential for reasoning about semantics preserving program transformations such as compiler optimizations. We adapt Lassen’s normal form bisimulations technique to establish the soundness of equational theories for both an untyped call-by-value \(\lambda \)-calculus and a variant of Levy’s call-by-push-value language. We demonstrate that our equational theory significantly simplifies the verification of optimizations.
C. Rizkallah—Work done while at University of Pennsylvania
This work is supported by NSF grant 1521539. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF.
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
Similar content being viewed by others
References
Abramsky, S.: The lazy \(\lambda \)- calculus. In: Research Topics in Functional Programming, pp. 65–116. Addison Wesley (1990)
Abramsky, S., Ong, C.H.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993)
Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Elsevier Science, New York (2013)
Biernacki, D., Lenglet, S., Polesiuk, P.: Proving soundness of extensional normal-form bisimilarities. In: Mathematical Foundations of Program Semantics (MFPS). Electronic Notes in Theoretical Computer Science (2017)
Crary, K.: A simple proof of call-by-value standardization. Technical report CMU-CS-09-137, Carnegie Mellon University (2009). https://www.cs.cmu.edu/~crary/papers/2009/standard.pdf
Downen, P., Maurer, L., Ariola, Z.M., Jones, S.P.: Sequent calculus as a compiler intermediate language. In: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 74–88 (2016)
Garbuzov, D., Mansky, W., Rizkallah, C., Zdancewic, S.: Structural operational semantics for control flow graph machines. CoRR abs/1805.05400 (2018). http://arxiv.org/abs/1805.05400
Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: Cakeml: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 179–191. ACM, New York (2014). https://doi.org/10.1145/2535838.2535841, http://doi.acm.org/10.1145/2535838.2535841
Lassen, S.B.: Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. Electron. Notes Theor. Comput. Sci. 20, 346–374 (1999)
Lassen, S.B.: Eager normal form bisimulation. In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), pp. 345–354 (2005)
Leroy, X.: A formally verified compiler back-end. J. Autom. Reasoning 43(4), 363–446 (2009). https://doi.org/10.1007/s10817-009-9155-4
Levy, P.B.: Call-by-push-value: a subsuming paradigm. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 228–243. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48959-2_17
Mason, I., Talcott, C.: Equivalence in functional languages with effects. J. Funct. Program. 1(3), 287–327 (1991)
Maurer, L., Downen, P., Ariola, Z.M., Peyton Jones, S.: Compiling without continuations. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 482–494. ACM (2017)
Morris, J.H.: Lambda calculus models of programming languages. Ph.D. thesis, Massachusets Institute of Technology (1968)
Rizkallah, C., Garbuzov, D., Zdancewic, S.: Accompanying Coq formalization (2018). http://www.cse.unsw.edu.au/~crizkallah/publications/equational_theory_cbpv.tar.gz
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, pp. 293–302. IEEE (2007)
Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120–127 (1995). https://doi.org/10.1006/inco.1995.1057
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Appendix: Definition of \(\mathcal {P}\) for CBPV
A Appendix: Definition of \(\mathcal {P}\) for CBPV
Rules defining conditional compatible closure \(\mathcal {P}\) of a (binary) relation R and a (unary) predicate P.
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Rizkallah, C., Garbuzov, D., Zdancewic, S. (2018). A Formal Equational Theory for Call-By-Push-Value. In: Avigad, J., Mahboubi, A. (eds) Interactive Theorem Proving. ITP 2018. Lecture Notes in Computer Science(), vol 10895. Springer, Cham. https://doi.org/10.1007/978-3-319-94821-8_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-94821-8_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94820-1
Online ISBN: 978-3-319-94821-8
eBook Packages: Computer ScienceComputer Science (R0)