Research on Computable Analysis and Verification of Efficient Exact Real Computation

• Project/Area Number: 24K20735
• Research Category: Grant-in-Aid for Early-Career Scientists
• Allocation Type: Multi-year Fund
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: Kyoto University
• Principal Investigator: THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
• Project Period (FY): 2024-04-01 – 2029-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000); Fiscal Year 2028: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2027: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2026: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
• Keywords: 計算可能解析学 / 微分方程式 / 精度保証付き数値計算 / 計算機援用証明

Outline of Research at the Start

he main purpose of the project is to apply and extend ideas from computable analysis to verified and efficient exact computation over uncountable mathematical structures based on strong theoretical foundations and its formal verification using proof assistants.
The project not only aims for theoretical correctness results but also for efficiency in terms of resource usage and for usability in practical applications. Additionally to empiric evaluation of algorithms by experiments, efficiency is also studied systematically in form of complexity theory.