Towards efficient solvers for ordinary differential equations in exact real arithmetic
| Project/Area Number |
18J10407
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
THIES HOLGER 九州大学, システム情報科学研究院, 助教
|
|---|
| Project Period (FY) |
2018-04-25 – 2020-03-31
|
| Project Status |
Completed (Fiscal Year 2019)
|
| Budget Amount *help |
¥1,900,000 (Direct Cost: ¥1,900,000)
Fiscal Year 2019: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2018: ¥1,000,000 (Direct Cost: ¥1,000,000)
|
|---|
| 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 |
令和元年度が最終年度であるため、記入しない。
|
Report
(2 results)
Research Products
(17 results)
-
[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
Related Report
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
