Regular Language Representations in Coq

View the project on GitHub

About

Welcome to the Regular Language Representations in Coq project website! This project is part of coq-community.

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.

This is an open source project, licensed under CeCILL-B.

Get the code

The current stable release of Regular Language Representations in Coq can be downloaded from GitHub.

Documentation

The coqdoc presentations of releases can be browsed online:

• v1.1.1
• v1.1

See also related publications:

• Regular Language Representations in the Constructive Type Theory of Coq doi:10.1007/s10817-018-9460-x

Help and contact

• Report issues on GitHub
• Chat with us on Zulip
• Discuss with us on Coq’s Discourse forum

Authors and contributors

• Christian Doczkal
• Jan-Oliver Kaiser
• Gert Smolka