Automatic Complexity Analysis for programs extracted from Coq proofs
We describe an automatic complexity analysis mechanism for programs
extracted from proofs carried out with the proof assistant Coq. By
extraction, we mean the automatic generation of MiniML programs. By
complexity analysis, we mean the automatic generation of a
description of the time-complexity of a MiniML program in terms of
the number of steps needed for its execution. This description can be
a natural number for \emph{closed program}, that is, programs coming
along with their actual inputs. For programs per se, the description
is given in terms of a set of recurrence relations which relate the
number of steps of a computation to the size of the
inputs. Going from these recurrence relation to actual complexity
functions is a hard task that requires the use of sophisticated tools
for symbolic computations.