package coq-reglang
Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp
Install
Dune Dependency
Authors
Maintainers
Sources
reglang-1.2.2.tar.gz
sha512=d30ceffa9e087b8bf84a578a3b85732a1ac84d70b316b3f9666b6ef93b4884d020d5a2efba054295cf47e8c3da3249bd07d5721c82f809a96ad75bcc1804a756
Description
This library provides definitions and verified translations between different representations of regular languages: various forms of automata (deterministic, nondeterministic, one-way, two-way), regular expressions, and the logic WS1S. It also contains various decidability results and closure properties of regular languages.
Tags
category:Computer Science/Formal Languages Theory and Automata keyword:regular languages keyword:regular expressions keyword:finite automata keyword:two-way automata keyword:monadic second-order logic logpath:RegLang date:2024-01-19Published: 10 May 2025
Dependencies (3)
-
coq-hierarchy-builder
>= "1.4.0" -
coq-mathcomp-ssreflect
>= "2.0" & < "2.5" -
coq
>= "8.16" & < "9.1~"
Dev Dependencies
None
Used by (1)
-
coq-regexp-brzozowski
>= "1.2"
Conflicts
None
On This Page