package coq-regexp-brzozowski

  1. Overview
  2. No Docs
Decision procedures for regular expression equivalence in Coq using Mathematical Components

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. T
    Thierry Coquand
  2. V
    Vincent Siles

Maintainers

  1. P
    palmskog@gmail.com

Sources

v1.2.tar.gz
sha512=425ca64ee3b89c4be556c1a522866650e4925b373899e8456dbdda58045eb9537914bffe12a940b341d6716ac60fec247c6b467747cd4302353433e369ca3cc2

Description

Coq library that formalizes decision procedures for regular expression equivalence, using the Mathematical Components library. The formalization builds on Brzozowski's derivatives of regular expressions for correctness.

Tags

category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Computer Science/Formal Languages Theory and Automata keyword:regular expressions keyword:decision procedure keyword:relation algebra logpath:RegexpBrzozowski date:2023-10-14

Published: 14 Oct 2023

Dependencies (3)

  1. coq-reglang >= "1.2.0"
  2. coq-mathcomp-ssreflect >= "2.0"
  3. coq >= "8.16"

Dev Dependencies

None

Used by

None

Conflicts

None