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.8.0.tar.gz
md5=7dfb0acdf48885cf2c41881e303865d9

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: 06 Feb 2019

Dependencies (2)

  1. coq >= "8.8" & < "8.9~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None