package coq-reglang

  1. Overview
  2. No Docs
Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp

Install

Dune Dependency

github.com Edit opam file Versions (7)

Authors

  1. C
    Christian Doczkal
  2. J
    Jan-Oliver Kaiser
  3. G
    Gert Smolka

Maintainers

  1. P
    palmskog@gmail.com

Sources

reglang-1.2.1.tar.gz
sha512=d8eca6d395e302f408e8dcab16093f4561f0059eab4302af94ade7a6de904642b77d8ce2beb0307db54e1ceada9977faa7d1ddfb1f73423dc2e1b9476b138e33

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-19

Published: 19 Jan 2024

Dependencies (3)

  1. coq-hierarchy-builder >= "1.4.0"
  2. coq-mathcomp-ssreflect >= "2.0" & < "2.4"
  3. coq >= "8.16" & < "8.21"

Dev Dependencies

None

Used by (1)

  1. coq-regexp-brzozowski >= "1.2"

Conflicts

None