A verified certificate checker running in ML. For large numbers I found out that the checking actually runs very fast, so after all LCF would be maybe possible. I use external software to find primary number decomposition and this takes the most of the time.
Actually for the example I sent, it does not terminate on my machine and I was forced to give the primenumber decomposition for the first step (the rest works). I can sent the sources to test with your oracle, but I used some tricks for Code-generation too, so maybe it's not trivial. Aemin. Steven Obua wrote: > Amine Chaieb wrote: > >> LCF? are you kidding? >> >> > So how did you do it then ? How long did the check run? Where can I find > the sources? > > Steven
