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.
David Pereira (email), Nelma Moreira and Simao Melo de Sousa
Last update: 25 of February, 2013