Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics

Mallku Soldevila, Rodrigo Ribeiro, Beta Ziliani

TL;DR

The paper presents a toolchain for translating Redex models into Coq using a shallow embedding of Redex semantics, enabling certified verification of reduction semantics properties. Building on Klein et al.'s RedexK, it proves termination of the matching/decomposition algorithm via a well-founded, primitive-recursive formulation and establishes soundness and correspondence with the original semantics. It further adapts RedexK to support future Redex features such as Kleene closure of patterns and develops Coq tactics to automate certifications. This work lays the groundwork for automated transpilation of Redex models into Coq and opens avenues for decidability-focused tooling in semantics engineering.

Abstract

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.

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics

TL;DR

The paper presents a toolchain for translating Redex models into Coq using a shallow embedding of Redex semantics, enabling certified verification of reduction semantics properties. Building on Klein et al.'s RedexK, it proves termination of the matching/decomposition algorithm via a well-founded, primitive-recursive formulation and establishes soundness and correspondence with the original semantics. It further adapts RedexK to support future Redex features such as Kleene closure of patterns and develops Coq tactics to automate certifications. This work lays the groundwork for automated transpilation of Redex models into Coq and opens avenues for decidability-focused tooling in semantics engineering.

Abstract

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.
Paper Structure (14 sections, 6 figures)

This paper contains 14 sections, 6 figures.

Table of Contents

  1. Introduction
  2. Motivation
  3. Summary of the contributions.
  4. Redex
  5. Expressing Redex in Coq.
  6. Language of terms and patterns
  7. Symbols
  8. Terms
  9. Patterns
  10. Decidability of predicates about terms and patterns
  11. Grammars
  12. Remaining data-structures
  13. Matching and decomposition
  14. Well-founded relation over the domain of matching/decomposition

Figures (6)

  • Figure 1: Definition of a language in Redex.
  • Figure 2: Definition of a meta-function in Redex: free variable in $\lambda$ terms.
  • Figure 3: Definition of a semantics relation in Redex.
  • Figure 4: A module type capturing assumptions about several atomic elements of the grammar.
  • Figure 5: Language of terms.
  • ...and 1 more figures

Theorems & Definitions (1)

  • definition thmcounterdefinition: Left-recursion semcontext