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

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:2018-09-18

Published: 24 Feb 2020

Dependencies (2)

  1. coq-mathcomp-ssreflect >= "1.6" & < "1.8~"
  2. coq >= "8.6" & < "8.10~"

Dev Dependencies

None

Used by

None

Conflicts

None