package coq-regexp-brzozowski

  1. Overview
  2. No Docs
Decision procedures for regular expression equivalence in Coq using Mathematical Components

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. T
    Thierry Coquand
  2. V
    Vincent Siles

Maintainers

  1. P
    palmskog@gmail.com

Sources

v1.0.tar.gz
sha512=bc837c5c76ec5e6751fcff7f00bf5fffbfb4ad53ca4212f259f2d61f61df65efd588c97fcb5ce45a6eec3e4f2339a2cf06ca1977d1d13569b0fec856d3522a02

Description

Coq library that formalizes decision procedures for regular expression equivalence, using the Mathematical Components library. The formalization builds on Brzozowski's derivatives of regular expressions for correctness.

Tags

category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Computer Science/Formal Languages Theory and Automata keyword:regular expressions keyword:decision procedure keyword:relation algebra logpath:RegexpBrzozowski date:2022-01-22

Published: 21 Jan 2022

Dependencies (3)

  1. coq-reglang >= "1.1.3" & < "1.2.0"
  2. coq-mathcomp-ssreflect >= "1.12.0" & < "1.16.0"
  3. coq >= "8.10" & < "8.17~"

Dev Dependencies

None

Used by

None

Conflicts

None