Document Open Access Logo

Generalized Refocusing: From Hybrid Strategies to Abstract Machines

Authors Malgorzata Biernacka, Witold Charatonik, Klara Zielinska

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.10.pdf
  • Filesize: 495 kB
  • 17 pages

Document Identifiers

Author Details

Malgorzata Biernacka
Witold Charatonik
Klara Zielinska

Cite AsGet BibTex

Malgorzata Biernacka, Witold Charatonik, and Klara Zielinska. Generalized Refocusing: From Hybrid Strategies to Abstract Machines. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.FSCD.2017.10

Abstract

We present a generalization of the refocusing procedure that provides a generic method for deriving an abstract machine from a specification of a reduction semantics satisfying simple initial conditions. The proposed generalization is applicable to a class of reduction semantics encoding hybrid strategies as well as uniform strategies handled by the original refocusing method. The resulting machine is proved to correctly trace (i.e., bisimulate in smaller steps) the input reduction semantics. The procedure and the correctness proofs have been formalized in the Coq proof assistant.
Keywords
  • reduction semantics
  • abstract machines
  • formal verification
  • Coq

Metrics

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

References

  1. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Dale Miller, editor, Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'03), pages 8-19, Uppsala, Sweden, August 2003. ACM Press. Google Scholar
  2. Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1(2:5):1-39, November 2005. Google Scholar
  3. Małgorzata Biernacka and Olivier Danvy. A syntactic correspondence between context-sensitive calculi and abstract machines. Theoretical Computer Science, 375(1-3):76-108, 2007. Google Scholar
  4. Pierre Crégut. Strongly reducing variants of the Krivine abstract machine. Higher-Order and Symbolic Computation, 20(3):209-230, 2007. A preliminary version was presented at the 1990 ACM Conference on Lisp and Functional Programming. Google Scholar
  5. Olivier Danvy. Defunctionalized interpreters for programming languages. In Peter Thiemann, editor, Proceedings of the 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP'08), SIGPLAN Notices, Vol. 43, No. 9, Victoria, British Columbia, September 2008. ACM, ACM Press. Invited talk. Google Scholar
  6. Olivier Danvy and Jacob Johannsen. From outermost reduction semantics to abstract machine. In Gopal Gupta and Ricardo Peña, editors, 23rd International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2013, pages 91-98. Springer-VS, 2014. URL: http://dx.doi.org/10.1007/978-3-319-14125-1.
  7. Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. Research Report BRICS RS-04-26, DAIMI, Department of Computer Science, Aarhus University, Aarhus, Denmark, November 2004. A preliminary version appeared in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science, Vol. 59.4. Google Scholar
  8. Matthias Felleisen. The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Computer Science Department, Indiana University, Bloomington, Indiana, August 1987. Google Scholar
  9. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. The MIT Press, 1st edition, 2009. Google Scholar
  10. Ronald Garcia, Andrew Lumsdaine, and Amr Sabry. Lazy evaluation and delimited control. In Benjamin C. Pierce, editor, Proceedings of the Thirty-Fifth Annual ACM Symposium on Principles of Programming Languages, pages 153-164. ACM Press, January 2009. Google Scholar
  11. A García-Pérez and Pablo Nogueira. On the syntactic and functional correspondence between hybrid (or layered) normalisers and abstract machines. Science of Computer Programming, 95:176-199, 2014. Google Scholar
  12. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Simon Peyton Jones, editor, Proceedings of the 2002 ACM SIGPLAN International Conference on Functional Programming (ICFP'02), SIGPLAN Notices, Vol. 37, No. 9, pages 235-246, Pittsburgh, Pennsylvania, September 2002. ACM, ACM Press. Google Scholar
  13. Thérèse Hardin, Luc Maranget, and Bruno Pagano. Functional runtime systems within the lambda-sigma calculus. Journal of Functional Programming, 8(2):131-172, 1998. Google Scholar
  14. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007. Google Scholar
  15. Grigore Roşu and Traian Florin Şerbănuţă. An overview of the K semantic framework. Journal of Logic and Algebraic Programming, 79(6):397-434, 2010. URL: http://dx.doi.org/10.1016/j.jlap.2010.03.012.
  16. Peter Sestoft. Demonstrating lambda calculus reduction. In Torben Æ. Mogensen, David A. Schmidt, and I. Hal Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, number 2566 in Lecture Notes in Computer Science, pages 420-435. Springer-Verlag, 2002. Google Scholar
  17. Filip Sieczkowski, Małgorzata Biernacka, and Dariusz Biernacki. Automating derivations of abstract machines from reduction semantics: a generic formalization of refocusing in Coq. In Juriaan Hage and Marco T. Morazán, editors, The 22nd International Conference on Implementation and Application of Functional Languages (IFL 2010), number 6647 in Lecture Notes in Computer Science, pages 72-88, Alphen aan den Rijn, The Netherlands, September 2010. Springer-Verlag. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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