PDCoq

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