Home

Awesome

Regular Language Representations in the Constructive Type Theory of Coq

This repository contains the Coq development accompanying the paper:

Christian Doczkal and Gert Smolka, Regular Language Representations in the Constructive Type Theory of Coq, J. Autom. Reason. - Special Issue on Milestones in Interactive Theorem Proving, Springer, 2018.

Prerequisites

One of the following:

Building and Installation

The easiest way to install the library is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-reglang

To instead build and install the library manually, run make followed by make install.

HTML Documentation

To generate the HTML documentation, run make website and point your browser at website/toc.html

Pregenerated HTML documentation (and a pre-print of the paper) can be found at: https://www.ps.uni-saarland.de/extras/RLR-Coq

File Contents