-
Notifications
You must be signed in to change notification settings - Fork 7
/
meta.yml
125 lines (105 loc) · 3.58 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
---
fullname: Regular Language Representations in Coq
shortname: reglang
organization: coq-community
community: true
action: true
nix: false
coqdoc: true
dune: true
doi: 10.1007/s10817-018-9460-x
synopsis: >-
Representations of regular languages (i.e., regexps, various types
of automata, and WS1S) with equivalence proofs, in Coq and MathComp
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.
publications:
- pub_url: https://hal.archives-ouvertes.fr/hal-01832031/document
pub_title: Regular Language Representations in the Constructive Type Theory of Coq
pub_doi: 10.1007/s10817-018-9460-x
authors:
- name: Christian Doczkal
initial: true
- name: Jan-Oliver Kaiser
initial: true
- name: Gert Smolka
initial: true
maintainers:
- name: Christian Doczkal
nickname: chdoc
- name: Karl Palmskog
nickname: palmskog
opam-file-maintainer: palmskog@gmail.com
opam-file-version: dev
license:
fullname: CeCILL-B
identifier: CECILL-B
supported_coq_versions:
text: 8.16 or later (use releases for other Coq versions)
opam: '{>= "8.16"}'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "2.0"}'
description: |-
[MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
- opam:
name: coq-hierarchy-builder
version: '{>= "1.4.0"}'
description: |-
[Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later
tested_coq_opam_versions:
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.16'
repo: 'mathcomp/mathcomp'
ci_cron_schedule: '10 1 * * 0'
namespace: RegLang
keywords:
- name: regular languages
- name: regular expressions
- name: finite automata
- name: two-way automata
- name: monadic second-order logic
categories:
- name: Computer Science/Formal Languages Theory and Automata
documentation: |-
## HTML Documentation
To generate HTML documentation, run `make coqdoc` and point your browser at `docs/coqdoc/toc.html`.
See also the pregenerated HTML documentation for the [latest release](https://coq-community.org/reglang/docs/latest/coqdoc/toc.html).
## File Contents
* `misc.v`, `setoid_leq.v`: basic infrastructure independent of regular languages
* `languages.v`: languages and decidable languages
* `dfa.v`:
* results on deterministic one-way automata
* definition of regularity
* criteria for nonregularity
* `nfa.v`: Results on nondeterministic one-way automata
* `regexp.v`: Regular expressions and Kleene Theorem
* `minimization.v`: minimization and uniqueness of minimal DFAs
* `myhill_nerode.v`: classifiers and the constructive Myhill-Nerode theorem
* `two_way.v`: deterministic and nondeterministic two-way automata
* `vardi.v`: translation from 2NFAs to NFAs for the complement language
* `shepherdson.v`: translation from 2NFAs and 2DFAs to DFAs (via classifiers)
* `wmso.v`:
* decidability of WS1S
* WS1S as representation of regular languages
---