Redex -> Coq: towards a theory of decidability of Redex's reduction semantics
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910318996750336 |
|---|---|
| author | Soldevila, Mallku Ribeiro, Rodrigo Ziliani, Beta |
| author_facet | Soldevila, Mallku Ribeiro, Rodrigo Ziliani, Beta |
| contents | We propose the first steps in the development of a tool to automate the translation of Redex models into a (hopefully) semantically equivalent model in Coq, and to provide tactics to help in the certification of fundamental properties of such models. The work is heavily based on a model of Redex's semantics developed by Klein et al. By means of a simple generalization of the matching problem in Redex, we obtain an algorithm suitable for its mechanization in Coq, for which we prove its soundness properties and its correspondence with the original solution proposed by Klein et al. In the process, we also adequate some parts of our mechanization to better prepare it for the future inclusion of Redex features absent in the present model, like its Kleene-star operator. Finally, we discuss future avenues of development that are enabled by this work. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_03488 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Redex -> Coq: towards a theory of decidability of Redex's reduction semantics Soldevila, Mallku Ribeiro, Rodrigo Ziliani, Beta Logic in Computer Science Programming Languages We propose the first steps in the development of a tool to automate the translation of Redex models into a (hopefully) semantically equivalent model in Coq, and to provide tactics to help in the certification of fundamental properties of such models. The work is heavily based on a model of Redex's semantics developed by Klein et al. By means of a simple generalization of the matching problem in Redex, we obtain an algorithm suitable for its mechanization in Coq, for which we prove its soundness properties and its correspondence with the original solution proposed by Klein et al. In the process, we also adequate some parts of our mechanization to better prepare it for the future inclusion of Redex features absent in the present model, like its Kleene-star operator. Finally, we discuss future avenues of development that are enabled by this work. |
| title | Redex -> Coq: towards a theory of decidability of Redex's reduction semantics |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2402.03488 |