coq-founify

Correctness and extraction of the unification algorithm. A notion of terms based on symbols without fixed arities is defined and an extended unification problem is proved solvable on these terms. An algorithm, close from Robinson algorithm, can be extracted from the proof.

opam install coq-founify.8.5.0
homepage
https://github.com/coq-contribs/founify
license
Proprietary
bugs tracker
https://github.com/coq-contribs/founify/issues
dependencies
coq (>= 8.5 & < 8.6~) & camlp5
source
https://github.com/coq-contribs/founify/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-founify/coq-founify.8.5.0