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
|
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<meta charset="utf-8" />
<meta name="generator" content="pandoc" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
<title>Regular Language Representations in Coq</title>
<style type="text/css">
code{white-space: pre-wrap;}
span.smallcaps{font-variant: small-caps;}
span.underline{text-decoration: underline;}
div.column{display: inline-block; vertical-align: top; width: 50%;}
</style>
<style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
<style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
<style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
<style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
<style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
</head>
<body>
<header id="title-block-header">
<h1 class="title">Regular Language Representations in Coq</h1>
</header>
<div style="text-align:left">
<img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"> <a href="https://github.com/coq-community/reglang">View the project on GitHub</a> <img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
</div>
<h2 id="about">About</h2>
<p>Welcome to the Regular Language Representations in Coq project website! This project is part of <a href="https://github.com/coq-community/manifesto">coq-community</a>.</p>
<p>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.</p>
<p>This is an open source project, licensed under CeCILL-B.</p>
<h2 id="get-the-code">Get the code</h2>
<p>The current stable release of Regular Language Representations in Coq can be <a href="https://github.com/coq-community/reglang/releases">downloaded from GitHub</a>.</p>
<h2 id="documentation">Documentation</h2>
<p>The coqdoc presentations of releases can be browsed online:</p>
<ul>
<li><a href="docs/v1.1.1/coqdoc/toc.html">v1.1.1</a></li>
<li><a href="docs/v1.1/coqdoc/toc.html">v1.1</a></li>
</ul>
<p>See also related publications:</p>
<ul>
<li><a href="https://hal.archives-ouvertes.fr/hal-01832031/document">Regular Language Representations in the Constructive Type Theory of Coq</a> doi:<a href="https://doi.org/10.1007/s10817-018-9460-x">10.1007/s10817-018-9460-x</a></li>
</ul>
<h2 id="help-and-contact">Help and contact</h2>
<ul>
<li>Report issues on <a href="https://github.com/coq-community/reglang/issues">GitHub</a></li>
<li>Chat with us on <a href="https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users">Zulip</a></li>
<li>Discuss with us on Coq’s <a href="https://coq.discourse.group">Discourse</a> forum</li>
</ul>
<h2 id="authors-and-contributors">Authors and contributors</h2>
<ul>
<li>Christian Doczkal</li>
<li>Jan-Oliver Kaiser</li>
<li>Gert Smolka</li>
</ul>
</body>
</html>
|
