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

v1.1.3.tar.gz
sha512=45085423899a0957922198c24c54c496cc4d4f9f02bd9ed6db72854436982acc9994487b0381bad8046eec5be0252a6fdc2ef0f001e48a0f58c323f1e46ee143

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:2022-01-20

Published: 20 Jan 2022

Dependencies (2)

  1. coq-mathcomp-ssreflect >= "1.11" & < "1.20~"
  2. coq >= "8.10" & < "8.21~"

Dev Dependencies

None

Used by (1)

  1. coq-regexp-brzozowski < "1.2"

Conflicts

None