Least-fixed point semantics of partial recursive functions


 COMPILATION

Make sure that Coq and Ocaml are installed in your system. The following 
versions have been tested:
      Coq 8.2
      Ocaml 3.09.3

The makefile assumes that the directory of the Coq installation is /usr. If it
is located somewhere else on your system, correct the variable COQTOP in
Makefile.

Try executing

      make

and then

      ./perfsqrt <some integer>



 AUTHORS

Yves Bertot
Vladimir Komendantsky