DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2024.34

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

Authors: Mallku Soldevila, Rodrigo Ribeiro, and Beta Ziliani

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{soldevila_et_al:LIPIcs.ITP.2024.34,
  author =	{Soldevila, Mallku and Ribeiro, Rodrigo and Ziliani, Beta},
  title =	{{Redex2Coq: Towards a Theory of Decidability of Redex’s Reduction Semantics}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{34:1--34:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.34},
  URN =		{urn:nbn:de:0030-drops-207629},
  doi =		{10.4230/LIPIcs.ITP.2024.34},
  annote =	{Keywords: Coq, PLT Redex, Reduction semantics}
}

Search Results

Documents authored by Ribeiro, Rodrigo

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

Abstract

Cite as

Thanks for your feedback!

Could not send message