Deciding Regular Expression and KAT terms (In)Equivalence in Coq Through Partial Derivatives
Source code of the development (using the Coq proof assistant) for regular expressions:
Version 1.1 (compiles with Coq-8.3pl5) coqdoc (Pure Ltac tactic for deciding relation equations)
Version 1.2 (compiles with Coq-8.3pl5) coqdoc (Tactic for deciding relation equations using OCaml reification)
Version 1.3 (compiles with Coq-8.4pl1) coqdoc
Source code of the development (using the Coq proof assistant) for KAT terms:
Version 1.1 (compiles with Coq-8.4pl1)
All the available developments require the Containers (for Coq 8.3)(for Coq 8.4).
Here are the slides of a talk given about PDCoq at the RAMiCS conference.
Here is the final version of David Pereira's PhD thesis containing a detailed description of the above developments.
You can also consult some papers related to the developments carried out along the development of PDCoq:
David Pereira (email), Nelma Moreira and Simao Melo de Sousa
Last update: 25 of February, 2013
- A first paper that addresses an axiomatization of Kleene algebra with tests. No semantic model is considered here.
- A paper presented at CIAA 2010 describing the proof of the validity of the partial derivative automata.
- A final paper presented at RAMIC 2012 where the certified decision procedure for regular expressions equivalence is addressed.