Towards efficient solvers for ordinary differential equations in exact real arithmetic

在项目的第一年，一些关于ODE求解计算复杂度的理论结果可以得到改进。今年的主要目标是在项目更实际的方面取得进展，更具体地说，是在coq证明助手中从可计算分析中形式化算法。这种形式化是与欧洲的研究人员密切合作完成的，形式化的结果已经成为名为“Incone”的库的一部分，这是一个用于可计算分析的Coq库。作为第一个结果，一些更理论化的方面已经形式化了。部分工作已发表在第十届国际交互定理证明会议（ITP 2019）的论文集上。包含几个附加结果的较长版本也已被接受为期刊出版物。第二步考虑了更实际的方面。特别是，在Coq框架中开发了一个经过验证的无错误实数计算（精确实数计算）的实现。该实现的重点不仅是验证其正确性，而且要在效率方面与未经验证的精确实算术实现相媲美。上述工作还导致了关于精确实计算的语义和类型论环境下可计算分析的表述的一些新的理论结果。这项工作已经成为收入库的一部分，可以在网上找到。一些主要结果也已在论文中进行了总结，预计将很快发表。

In the first year of the project, some of the theoretical results on the computational complexity of ODE solving could be improved. The main goal of this year was to make progress on the more practical side of the project, more specifically on formalizing algorithms from computable analysis in the coq proof assistant.This formalization was done in close collaboration with researchers in Europe and the formalized results have been made part of a library called "Incone", a Coq library for computable analysis.As a first result, some more theoretical aspects have been formalized. Part of the work has been published in the proceedings of the 10th International Conference on Interactive Theorem Proving (ITP 2019).A longer version containing several additional results has also been accepted as a journal publication.In a second step more practical facets have been considered. In particular, a verified implementation of error-free real number computation (exact real computation) was developed in the Coq framework. The focus of this implementation was to not only verify its correctness, but also be comparable to non-verified implementations of exact real arithmetic in terms of efficiency.The above work also lead to some new theoretical results regarding the semantics of exact real computation and the formulation of computable analysis in a type-theoretic setting. The work has been made part of the incone library which can be found online. Some of the main results have also been summarized in papers and are expected to be published soon.