package coq-regexp-brzozowski
Decision procedures for regular expression equivalence in Coq using Mathematical Components
Install
Dune Dependency
Authors
Maintainers
Sources
v1.2.tar.gz
sha512=425ca64ee3b89c4be556c1a522866650e4925b373899e8456dbdda58045eb9537914bffe12a940b341d6716ac60fec247c6b467747cd4302353433e369ca3cc2
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-14Published: 14 Oct 2023
Dependencies (3)
-
coq-reglang
>= "1.2.0" -
coq-mathcomp-ssreflect
>= "2.0" -
coq
>= "8.16"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page