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>

Maintainers

  1. M
    matej.kosik@inria.fr

Sources

v8.5.0.tar.gz
md5=3cc50a91012a0c2cc6963ecff18dd5c2

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 Jun 2016

Dependencies (2)

  1. coq >= "8.5" & < "8.6~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None