coq-reglang

Regular Language Representations in the Constructive Type Theory of Coq We verify translations between different representations of regular languages: various forms of automata (deterministic, nondeterministic, one-way, two-way), regular expressions, and the logic WS1S. We also show various decidability results and closure properties.

opam install coq-reglang.1
homepage
https://github.com/chdoc/coq-reglang
license
CeCILL-B
bugs tracker
https://github.com/chdoc/coq-reglang/issues
dependencies
coq (>= 8.6 & < 8.9~) & coq-mathcomp-ssreflect (>= 1.6 & < 1.8~)
source
https://github.com/chdoc/coq-reglang/archive/v1.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-reglang/coq-reglang.1