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.1.tar.gz
sha512=d59a65aa9360e1e9de3f3bf777de04db422ffa6bc531e3f0eb2b6f4572c4fe2253a2b6fe36212c3e6edf80fa907f3c5d7070a6c2fba7f7a7ffc2d2eefed0874d

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:2023-10-14

Published: 14 Oct 2023

Dependencies (3)

  1. coq-reglang >= "1.1.3" & < "1.2.0"
  2. coq-mathcomp-ssreflect >= "1.13.0" & < "1.19"
  3. coq >= "8.11" & < "8.19~"

Dev Dependencies

None

Used by

None

Conflicts

None