package coq-regexp

  1. Overview
  2. No Docs
Regular Expression

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. T
    Takashi Miyamoto <tmiya@bu.iij4u.or.jp> [http://study-func-prog.blogspot.com/]

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.10.0.tar.gz
md5=faf3b343baa5389f443020f538029a0a

Description

The Library RegExp is a Coq library for regular expression. The implementation is based on the Janusz Brzozowski's algorithm ("Derivatives of Regular Expressions", Journal of the ACM 1964). The RegExp library satisfies the axioms of Kleene Algebra. The proofs are shown in the library.

Tags

keyword: regular expressions keyword: Kleene algebra category: Computer Science/Formal Languages Theory and Automata

Published: 07 Dec 2019

Dependencies (2)

  1. coq >= "8.10" & < "8.11~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None