Skip to main content
SpringerLink
Log in
Book cover

International Conference on Interactive Theorem Proving

ITP 2018: Interactive Theorem Proving pp 523–541Cite as

A Formal Equational Theory for Call-By-Push-Value

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10895))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Abramsky, S.: The lazy \(\lambda \)- calculus. In: Research Topics in Functional Programming, pp. 65–116. Addison Wesley (1990)

    Google Scholar 

  2. Abramsky, S., Ong, C.H.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993)

    Article  MathSciNet  Google Scholar 

  3. Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Elsevier Science, New York (2013)

    Book  Google Scholar 

  4. 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)

    Google Scholar 

  5. 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

  6. 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)

    Google Scholar 

  7. 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

  8. 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

  9. 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)

    Article  MathSciNet  Google Scholar 

  10. Lassen, S.B.: Eager normal form bisimulation. In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), pp. 345–354 (2005)

    Google Scholar 

  11. 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

    Article  MathSciNet  MATH  Google Scholar 

  12. 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

    Chapter  Google Scholar 

  13. Mason, I., Talcott, C.: Equivalence in functional languages with effects. J. Funct. Program. 1(3), 287–327 (1991)

    Article  MathSciNet  Google Scholar 

  14. 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)

    Google Scholar 

  15. Morris, J.H.: Lambda calculus models of programming languages. Ph.D. thesis, Massachusets Institute of Technology (1968)

    Google Scholar 

  16. Rizkallah, C., Garbuzov, D., Zdancewic, S.: Accompanying Coq formalization (2018). http://www.cse.unsw.edu.au/~crizkallah/publications/equational_theory_cbpv.tar.gz

  17. 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)

    Google Scholar 

  18. Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120–127 (1995). https://doi.org/10.1006/inco.1995.1057

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of New South Wales, Sydney, Australia

    Christine Rizkallah

  2. University of Pennsylvania, Philadelphia, USA

    Dmitri Garbuzov & Steve Zdancewic

Authors
  1. Christine Rizkallah
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dmitri Garbuzov
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Steve Zdancewic
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Christine Rizkallah .

Editor information

Editors and Affiliations

  1. Carnegie Mellon University, Pittsburgh, PA, USA

    Jeremy Avigad

  2. Inria, Nantes, France

    Assia Mahboubi

A Appendix: Definition of \(\mathcal {P}\) for CBPV

A Appendix: Definition of \(\mathcal {P}\) for CBPV

Fig. 11.
figure 11

Rules defining conditional compatible closure \(\mathcal {P}\) of a (binary) relation R and a (unary) predicate P.

Full size image

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation