2019 Fiscal Year Annual Research Report
Towards efficient solvers for ordinary differential equations in exact real arithmetic
| Project/Area Number |
18J10407
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
THIES HOLGER 九州大学, システム情報科学研究院, 助教
|
|---|
| Project Period (FY) |
2018-04-25 – 2020-03-31
|
| Keywords | 計算理論 / 計算量理論 / 計算可能解析 / 実数の計算理論 / 計算機援用証明 |
|---|
| Outline of Annual Research Achievements |
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.
|
| Research Progress Status |
令和元年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和元年度が最終年度であるため、記入しない。
|
-
[Journal Article] Quantitative Continuity and Computable Analysis in Coq2019
Author(s)
Florian Steinberg, Laurent Thery, Holger Thies
-
Journal Title
Proc. of the 10th International Conference on Interactive Theorem Proving (ITP 2019), September 9-12, 2019, Portland, OR, USA, LIPIcs-Leibniz International Proceedings in Informatics
Volume: 141
Pages: 28:1-28:21
DOI
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
-
