Skip to main content
SpringerLink
Log in

Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11275))

Included in the following conference series:

Abstract

We formally verify an abstract machine for a call-by-value \(\lambda \)-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement approach starting with a naive stack machine with substitution. We then refine to a machine with closures, and finally to a machine with a heap providing structure sharing for closures. We prove the correctness of the three refinement steps with compositional small-step bottom-up simulations. There is an accompanying Coq development verifying all results.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

References

  1. Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 363–376 (2014)

    Google Scholar 

  2. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  3. Biernacka, M., Charatonik, W., Zielinska, K.: Generalized refocusing: from hybrid strategies to abstract machines. In: LIPIcs, vol. 84. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2017)

    Google Scholar 

  4. Biernacka, M., Danvy, O.: A concrete framework for environment machines. ACM Trans. Comput. Logic (TOCL) 9(1), 6 (2007)

    Article  MathSciNet  Google Scholar 

  5. Cardelli, L.: Compiling a functional language. In: Proceedings of the 1984 ACM Symposium on LISP and Functional Programming, pp. 208–217. ACM (1984)

    Google Scholar 

  6. Cousineau, G., Curien, P.-L., Mauny, M.: The categorical abstract machine. Sci. Comput. Program. 8(2), 173–202 (1987)

    Article  MathSciNet  Google Scholar 

  7. Crégut, P.: An abstract machine for lambda-terms normalization. In: Proceedings of the 1990 ACM Conference on LISP and Functional Programming, pp. 333–340 (1990)

    Google Scholar 

  8. Dal Lago, U., Martini, S.: The weak lambda calculus as a reasonable machine. Theor. Comput. Sci. 398(1–3), 32–50 (2008)

    Article  MathSciNet  Google Scholar 

  9. Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. BRICS Rep. Ser. 11(26) (2004)

    Google Scholar 

  10. Felleisen, M., Friedman, D.P.: Control Operators, the SECD-machine, and the \(\lambda \)-calculus. Indiana University, Computer Science Department (1986)

    Google Scholar 

  11. Forster, Y., Kunze, F., Roth, M.: The strong invariance thesis for a \(\lambda \)-calculus. In: Workshop on Syntax and Semantics of Low-Level Languages (LOLA) (2017)

    Google Scholar 

  12. Forster, Y., Smolka, G.: Weak call-by-value lambda calculus as a model of computation in Coq. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 189–206. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_13

    Chapter  Google Scholar 

  13. Hardin, T., Maranget, L., Pagano, B.: Functional runtime systems within the lambda-sigma calculus. J. Funct. Programm. 8(2), 131–176 (1998)

    Article  MathSciNet  Google Scholar 

  14. Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6(4), 308–320 (1964)

    Article  Google Scholar 

  15. Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Technical report, INRIA (1990)

    Google Scholar 

  16. Leroy, X.: Functional programming languages, Part II: Abstract machines, the Modern SECD. Lectures on Functional Programming and Type Systems, MPRI course 2–4, slides and Coq developments (2016). https://xavierleroy.org/mpri/2-4/

  17. Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284–304 (2009)

    Article  MathSciNet  Google Scholar 

  18. Plotkin, G.D.: Call-by-name, call-by-value and the \(\lambda \)-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)

    Article  MathSciNet  Google Scholar 

  19. Ramsdell, J.D.: The tail-recursive SECD machine. J. Autom. Reason. 23(1), 43–62 (1999)

    Article  MathSciNet  Google Scholar 

  20. Rittri, M.: Proving the correctness of a virtual machine by a bisimulation. Licentiate thesis, Chalmers University and University of Göteborg (1988)

    Google Scholar 

  21. Swierstra, W.: From mathematics to abstract machine: a formal derivation of an executable Krivine machine. In: Proceedings Fourth Workshop on Mathematically Structured Functional Programming, pp. 163–177 (2012)

    Article  Google Scholar 

  22. The Coq Proof Assistant (2018). http://coq.inria.fr

Download references

Author information

Authors and Affiliations

  1. Saarland University, Saarbrücken, Germany

    Fabian Kunze, Gert Smolka & Yannick Forster

Authors
  1. Fabian Kunze
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gert Smolka
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yannick Forster
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Fabian Kunze , Gert Smolka or Yannick Forster .

Editor information

Editors and Affiliations

  1. Korea Advanced Institute of Science and Technology, Daejeon, Korea (Republic of)

    Sukyoung Ryu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kunze, F., Smolka, G., Forster, Y. (2018). Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. In: Ryu, S. (eds) Programming Languages and Systems. APLAS 2018. Lecture Notes in Computer Science(), vol 11275. Springer, Cham. https://doi.org/10.1007/978-3-030-02768-1_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02768-1_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02767-4

  • Online ISBN: 978-3-030-02768-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation