Document Open Access Logo

A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language

Authors Leonardo Rodríguez, Daniel Fridlender, Miguel Pagano

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2013.230.pdf
  • Filesize: 0.53 MB
  • 21 pages

Document Identifiers

Subject Classification

Keywords
  • Abstract Machines
  • Compiler Correctness
  • Big-step semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

In this paper we present a compiler that translates programs from an
imperative higher-order language into a sequence of instructions
for an abstract machine. We consider an extension of the Krivine machine for the call-by-name lambda calculus, which includes strict operators and imperative features. We show that the compiler is
correct with respect to the big-step semantics of our language, both
for convergent and divergent programs.

Cite As Get BibTex

Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano. A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 230-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.TYPES.2013.230

Author Details

Leonardo Rodríguez
Daniel Fridlender
Miguel Pagano

References

  1. Nick Benton and Chung-Kil Hur. Biorthogonality, step-indexing and compiler correctness. SIGPLAN Not., 44(9):97-108, August 2009. Google Scholar
  2. Yves Bertot. A certified compiler for an imperative language. Technical Report RR-3488, INRIA, September 1998. Google Scholar
  3. Yves Bertot. Theorem proving support in programming language semantics. CoRR, abs/0707.0926, 2007. Google Scholar
  4. Malgorzata Biernacka and Olivier Danvy. A concrete framework for environment machines. ACM Trans. Comput. Log., 9(1), 2007. Google Scholar
  5. Adam Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. SIGPLAN Not., 42(6):54-65, June 2007. Google Scholar
  6. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. SIGPLAN Not., 43(9):143-156, September 2008. Google Scholar
  7. Adam Chlipala. A verified compiler for an impure functional language. In POPL, pages 93-106, 2010. Google Scholar
  8. G. Cousineau and P.-L. Curien. The categorical abstract machine. Sci. Comput. Program., 8(2):173-202, April 1987. Google Scholar
  9. Pierre-Louis Curien. An abstract framework for environment machines. Theor. Comput. Sci., 82(2):389-402, 1991. Google Scholar
  10. Olivier Danvy and Lasse Nielsen. Refocusing in reduction semantics. Research report BRICS RS-04-26, DAIMI, Department of Computer Science, Aarhus University, Aarhus, Denmark, November 2004. Google Scholar
  11. Stephan Diehl and Peter Sestoft. Abstract machines for programming language implementation. Future Gener. Comput. Syst., 16(7):739-751, May 2000. Google Scholar
  12. Thérèse Hardin, Luc Maranget, and Bruno Pagano. Functional runtime systems within the lambda-sigma calculus. J. Funct. Program., 8(2):131-176, March 1998. Google Scholar
  13. Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In J. Gregory Morrisett and Simon L. Peyton Jones, editors, POPL, pages 141-152. ACM, 2006. Google Scholar
  14. Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher Order Symbol. Comput., 20(3):199-207, September 2007. Google Scholar
  15. P. J. Landin. The Mechanical Evaluation of Expressions. The Computer Journal, 6(4):308-320, January 1964. Google Scholar
  16. John Launchbury. Lazy imperative programming. In ACM Sigplan Workshop on State in Programming Languages, pages 46-56, 1993. (available as YALEU/DCS/RR968, Yale University). Google Scholar
  17. John Launchbury. A natural semantics for lazy evaluation. In POPL, pages 144-154, 1993. Google Scholar
  18. Xavier Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990. Google Scholar
  19. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. Google Scholar
  20. Xavier Leroy. A formally verified compiler back-end. J. Autom. Reason., 43(4):363-446, December 2009. Google Scholar
  21. Xavier Leroy. Mechanized semantics - with applications to program proof and compiler verification. In Logics and Languages for Reliability and Security, pages 195-224. IOS Press BV, 2010. Google Scholar
  22. Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Inf. Comput., 207(2):284-304, February 2009. Google Scholar
  23. Simon L. Peyton Jones. The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science). Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1987. Google Scholar
  24. Maciej Pirog and Dariusz Biernacki. A systematic derivation of the STG machine verified in Coq. SIGPLAN Not., 45(11):25-36, September 2010. Google Scholar
  25. John C. Reynolds. Using functor categories to generate intermediate code. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL'95, pages 25-36, New York, NY, USA, 1995. ACM. Google Scholar
  26. John C. Reynolds. The essence of Algol. In Peter W. O'Hearn and Robert D. Tennent, editors, ALGOL-like Languages, Volume 1, pages 67-88. Birkhauser Boston Inc., Cambridge, MA, USA, 1997. Google Scholar
  27. M. Rittri and Institutionen för informationsbehandling (Göteborg). Proving the Correctness of a Virtual Machine by a Bisimulation. Department of computer sciences, 1988. Google Scholar
  28. Peter Selinger. From continuation passing style to Krivine’s abstract machine. Manuscript, 2003. Available in Peter Selinger’s web site. Google Scholar
  29. Filip Sieczkowski, Małlgorzata Biernacka, and Dariusz Biernacki. Automating derivations of abstract machines from reduction semantics: A generic formalization of refocusing in Coq. In Proceedings of the 22Nd International Conference on Implementation and Application of Functional Languages, IFL'10, pages 72-88, Berlin, Heidelberg, 2011. Springer-Verlag. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact