A proof that Coq contains any total mu-recursive function
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
LICENSE_CeCILL_V2-en.txt
Makefile
README.md
_CoqProject
_config.yml
acc_utils.v
applications.v
cid.v
computable.v
coq_is_total.v
decidable_t.v
finite.v
list_utils.v
loop.v
minimizer.v
minimizer_bool.v
nat_minimizer.v
nat_utils.v
notations.v
pos.v
ra_bs.v
ra_ca.v
ra_ca_props.v
ra_rel.v
ra_sem_eq.v
recalg.v
recursor.v
tac_utils.v
tree.v
utils.v
vec.v

README.md

Coq contains any provably total mu-recursive function

This development is a proof in Coq that any mu-recursive function which defines a total predicate can be represented by a Coq term. It was developped under Coq 8.5pl3 but should also compile with Coq 8.6. This code will NOT compile under Coq 8.4 (see below).

To compile, type

make all

This code was developped by Dominique Larchey-Wendling and is distributed under the CeCILL Free Software License Agreement. It is complementary to the paper Typing Total Recursive Functions in Coq which was submitted to ITP'2017.

Starting from Coq 8.5, the syntax of pattern matching has changed. In particular, the constructor exist (for type sig X) now has 3 arguments instead of two. It is not possible to write code which is compatible for both Coq 8.4 and Coq 8.5.