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.2.tar.gz
sha512=13395112478648b7c0fa6ea7d54a535b53749c000b45b02ebb62a8ce503a0fd1ee637d1a04062740adccccb0b6f0832416b67b1c9e4ce32133eb5be568a669d3

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:2020-12-14

Published: 14 Jan 2021

Dependencies (2)

  1. coq-mathcomp-ssreflect >= "1.9" & < "1.15~"
  2. coq >= "8.10" & < "8.16~"

Dev Dependencies

None

Used by

None

Conflicts

None