| 研究実績の概要 |
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.
|
