Document Open Access Logo

Redex2Coq: Towards a Theory of Decidability of Redex’s Reduction Semantics

Authors Mallku Soldevila , Rodrigo Ribeiro , Beta Ziliani

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.34.pdf
  • Filesize: 0.78 MB
  • 18 pages

Document Identifiers

Author Details

Mallku Soldevila
  • FAMAF, UNC, Córdoba, Argentina
  • CONICET, Buenos Aires, Argentina
Rodrigo Ribeiro
  • DECOM, UFOP, Ouro Preto, Brazil
Beta Ziliani
  • FAMAF, UNC, Córdoba, Argentina
  • Manas.Tech, Buenos Aires, Argentina

Funding

  • Soldevila, Mallku: CONICET, Argentina.

Cite AsGet BibTex

Mallku Soldevila, Rodrigo Ribeiro, and Beta Ziliani. Redex2Coq: Towards a Theory of Decidability of Redex’s Reduction Semantics. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.34

Abstract

We propose the first step in the development of a tool to automate the translation of Redex models into a semantically equivalent model in Coq, and to provide tactics to help in the certification of fundamental properties of such models. The work is based on a model of Redex’s semantics developed by Klein et al. In this iteration, we were able to code in Coq a primitive recursive definition of the matching algorithm of Redex, and prove its correctness with respect to the original specification. The main challenge was to find the right generalization of the original algorithm (and its specification), and to find the proper well-founded relation to prove its termination. Additionally, we also adequate some parts of our mechanization to prepare it for the future inclusion of Redex features absent in Klein et al., such as the Kleene’s closure operator.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Rewrite systems
  • Theory of computation → Interactive proof systems
Keywords
  • Coq
  • PLT Redex
  • Reduction semantics

Metrics

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

Supplementary Materials

References

  1. Péter Bereczky, Xiaohong Chen, Dániel Horpácsi, Lucas Peña, and Jan Tušil. Mechanizing matching logic in coq. In Vlad Rusu, editor, Proceedings of the Sixth Working Formal Methods Symposium, "Al. I. Cuza University", Iasi, Romania, 19-20 September, 2022, volume 369 of Electronic Proceedings in Theoretical Computer Science, pages 17-36. Open Publishing Association, 2022. URL: https://doi.org/10.4204/EPTCS.369.2.
  2. Frédéric Blanqui and Adam Koprowski. Color: a coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Mathematical Structures in Computer Science, 21(4):827-859, 2011. URL: https://doi.org/10.1017/S0960129511000120.
  3. Brown PLT Group. Mechanized lambdajs. https://blog.brownplt.org/2012/06/04/lambdajs-coq.html, 2012.
  4. Steven Jaconette Casey Klein, Jay McCarthy and Robert Bruce Findler. A semantics for context-sensitive reduction semantics. In APLAS'11, 2011. Google Scholar
  5. M. Felleisen, R. B. Finlder, and M. Flatt. Semantics Engineering with PLT Redex. The MIT Press, 2009. Google Scholar
  6. A. Guha, C. Saftoiu, and S. Krishnamurthi. The essence of JavaScript. In ECOOP '10, 2010. Google Scholar
  7. Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. Run your research: On the effectiveness of lightweight mechanization. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '12, pages 285-296, New York, NY, USA, 2012. ACM. URL: https://doi.org/10.1145/2103656.2103691.
  8. Jacob Matthews and Robert Bruce Findler. An operational semantics for scheme. Journal of Functional Programming, 2007. Google Scholar
  9. Mark-Jan Nederhof and Giorgio Satta. The language intersection problem for non-recursive context-free grammars. Inf. Comput., 192(2):172-184, August 2004. URL: https://doi.org/10.1016/j.ic.2004.03.004.
  10. Lawrence C. Paulson. Constructing recursion operators in intuitionistic type theory. J. Symb. Comput., 2(4):325-355, December 1986. Google Scholar
  11. J. G. Politz, M. J. Carroll, B. S. Lerner, J. Pombrio, and S. Krishnamurthi. A tested semantics for getters, setters, and eval in JavaScript. In DLS '12, 2012. Google Scholar
  12. J. G. Politz, A. Martinez, M. Milano, S. Warren, D. Patterson, J. Li, A. Chitipothu, and S. Krishnamurthi. Python: The full monty: A tested semantics for the Python programming language. In OOPSLA '13, 2013. Google Scholar
  13. 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, 2010. Springer-Verlag. Google Scholar
  14. M. Soldevila, B. Ziliani, and B. Silvestre. From specification to testing: Semantics engineering for lua 5.2. Journal of Automated Reasoning, 2022. Google Scholar
  15. Mallku Soldevila, Rodrigo Ribeiro, and Beta Ziliani. redex2coq. Software, CONICET (Argentina), swhId: https://archive.softwareheritage.org/swh:1:dir:eea74f34ec4a10a6e7315b1d5d3f89327bce18a5;origin=https://github.com/Mallku2/redex2coq;visit=swh:1:snp:6b00934129869eda95d6e7403821644d2e9d683a;anchor=swh:1:rev:3722576c47b19be64fec7c188f6595ce8f5d1306 (visited on 2024-08-20). URL: https://github.com/Mallku2/redex2coq.
  16. Mallku Soldevila, Beta Ziliani, and Daniel Fridlender. Understanding Lua’s garbage collection: Towards a formalized static analyzer. In Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming, PPDP 2020, 2020. Google Scholar
  17. Mallku Soldevila, Beta Ziliani, Bruno Silvestre, Daniel Fridlender, and Fabio Mascarenhas. Decoding Lua: Formal semantics for the developer and the semanticist. In Proceedings of the 13th ACM SIGPLAN Dynamic Languages Symposium, DLS 2017, 2017. Google Scholar
  18. The Coq-std++ Team. An extended "standard library" for Coq, 2020. Available online at URL: https://gitlab.mpi-sws.org/iris/stdpp.
  19. Junfeng Xu. Redex-plus: a metanotation for programming languages. PhD thesis, University of British Columbia, 2023. URL: https://doi.org/10.14288/1.0435516.
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