Towards efficient solvers for ordinary differential equations in exact real arithmetic

在项目的第一年，关于常微分方程组求解计算复杂性的一些理论结果可以得到改进。今年的主要目标是在该项目更实用的方面取得进展，更具体地说是在辅助剂中从可计算分析中形式化算法。这种形式化是与欧洲的研究人员密切合作完成的，形式化的结果已经成为一个名为“INCONE”的库的一部分，这是一个用于计算分析的辅助库。作为第一个结果，一些更多的理论方面已经被形式化。部分工作已经在第十届交互定理证明国际会议(ITP 2019)上发表。包含几个额外结果的较长版本也被接受作为期刊发表。在第二步，考虑了更实际的方面。特别是，在CoQ框架中开发了一个经过验证的无误差实数计算(精确实数计算)实现。该实现的重点不仅在于验证其正确性，而且在效率上可以与未经验证的精确实数实现相媲美。上述工作还在精确实数计算的语义和类型论环境下的可计算分析公式方面得到了一些新的理论结果。这项工作已经成为inone图书馆的一部分，可以在网上找到。一些主要成果也已在论文中总结，预计很快就会发表。

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.