Skip to content
A proof of Stålmarck's algorithm in Coq [maintainer=@herbelin]
Coq OCaml Other
Branch: master
Clone or download

README.md

Stalmarck

Travis Contributing Code of Conduct Gitter DOI

A two-level approach to prove tautologies using Stålmarck's algorithm in Coq.

More details about the project can be found in the paper Formalizing Stålmarck's Algorithm in Coq.

Meta

  • Author(s):
    • Pierre Letouzey (initial)
    • Laurent Théry (initial)
  • Coq-community maintainer(s):
  • License: GNU Lesser General Public License v2.1 or later
  • Compatible Coq versions: Coq master (use the corresponding branch or release for other Coq versions)
  • Compatible OCaml versions: all versions supported by Coq
  • Additional dependencies: none

Building and installation instructions

The easiest way to install the latest released version is via OPAM:

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

To instead build and install manually, do:

git clone https://github.com/coq-community/stalmarck
cd stalmarck
make   # or make -j <number-of-cores-on-your-machine>
make install

After installation, the included modules are available under the Stalmarck namespace.

Documentation

This project is composed of:

  • a proof of correctness of the algorithm as described in "A Formalization of Stålmarck's Algorithm in Coq", TPHOLs2000.

  • an implementation of the algorithm. With respect to the paper, this implementation is completely functional and can be used inside Coq.

  • a reflected tactic staltac, that uses the extracted code to compute an execution trace; the trace checker is then called inside Coq.

See algoRun.v for examples how to use the algorithm inside Coq.

See StalTac_ex.v for examples how to use the reflected tactic.

WARNING: Stålmarck's method is patented and should not be used for commercial applications without the agreement of Prover Technology.

You can’t perform that action at this time.