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.tar.gz
sha512=e845e0b864c6d0ecde9dc21c47bd902b014b359d83694f6cecb55190581c5148ca06b13c0ec998feb24ebdcf18161c11b893de4df2ffbec02580a47b012acffd

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:2019-11-25

Published: 25 Nov 2019

Dependencies (2)

  1. coq-mathcomp-ssreflect >= "1.9" & < "1.12~"
  2. coq >= "8.7" & < "8.13~"

Dev Dependencies

None

Used by

None

Conflicts

None