View on GitHub


Supplementary material to "Continuous machines"

This webpage contains some information on how to access the Coq development for our paper “ Continuous and monotone machines”. The formal development has been made part of incone, a Coq library for computable analysis.

Installation instructions

You should have coq (8.9.0) running with the Coquelicot library (3.0) and from math-comp (1.9.0) the packages ssreflect and algebra.

The following libraries have to be installed in this order:

You can just clone this github repository using git clone --recurse-submodules, change into the top directory and run make to install all four libraries.

Alternatively if you are using opam you can also run opam install . --working-dir to install all necessary libraries.

The contents of the paper

Formal proofs of statements in the paper have been made part of the library and are scattered across several files and folders.

A good overview over how many of the main concepts from the paper are formalized can be ganed by looking at the example of representing real numbers using rational approximations (Example 2.2 in the paper) contained in examples/Q_reals.v in the incone library.

Further results and examples of the paper can be roughly related to the formalization as follows: