• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2023 年度 実績報告書

連続系における高階函数の保証つき厳密計算

研究課題

研究課題/領域番号 22KF0198
配分区分基金
研究機関京都大学

研究代表者

河村 彰星  京都大学, 数理解析研究所, 准教授 (20600117)

研究分担者 PARK SEWON  京都大学, 数理解析研究所, 外国人特別研究員
研究期間 (年度) 2023-03-08 – 2024-03-31
キーワードexact real computation / program verification / higher-order Hoare logic / constructive type theory / formalized mathematics
研究実績の概要

We have axiomatically formalized ERC in a mathematical language (which is a constructive type theory) such that the users' informative proofs get extracted to ERC programs that are certified to be correct. Our axiomatization provides an axiomatic type for exact real numbers and basic real number operations. It further provides a nondeterminism monad thus nondeterministic computation can be expressed and formally analyzed. We have implemented it in the Coq proof assistant and customized the extraction mechanism.

Taking this development in Coq as a formal system for studying the foundational aspect of the higher-order ERC computation, we have extended the work with higher-order objects such as (continuous) functions, subspaces, and fractals. We extend the above system with functions, and open, closed, compact and overt subsets that allow short and elegant proofs with computational content for various higher-order operations. From these proofs, we can also extract programs for testing inclusion, overlapping of sets, et cetera.

The lemmas proven in the system then guide us on how the operations should be provided in the language design. We provide an imperative programming language with higher-order pure functions and a nondeterministic limit operation whose semantics are then defined regarding the lemma that appeared in our Coq development. The formal semantics and sound proof rules are provided along with an example of nondeterministic root-finding and its correctness proof.

  • 研究成果

    (8件)

すべて 2024 2023 その他

すべて 国際共同研究 (1件) 雑誌論文 (2件) (うち国際共著 1件、 査読あり 2件、 オープンアクセス 1件) 学会発表 (5件) (うち国際学会 5件、 招待講演 1件)

  • [国際共同研究] マーストリヒト大学(オランダ)

    • 国名
      オランダ
    • 外国機関名
      マーストリヒト大学
  • [雑誌論文] Formalizing hyperspaces for extracting efficient exact real computation2023

    • 著者名/発表者名
      Michal Konecny;, Sewon Park, and Holger Thies
    • 雑誌名

      Leibniz International Proceedings in Informatics

      巻: 272 ページ: 59

    • DOI

      10.4230/LIPIcs.MFCS.2023.59

    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Verified exact real computation with nondeterministic functions and limits2023

    • 著者名/発表者名
      Park Sewon
    • 雑誌名

      Lecture Notes in Computer Science

      巻: 14292 ページ: 363~377

    • DOI

      10.1007/978-3-031-43587-4_26

    • 査読あり
  • [学会発表] Abstract data type for exact real numbers and verified computation2024

    • 著者名/発表者名
      Sewon Park
    • 学会等名
      17th International Conference on Computability, Complexity and Randomness (CCR2024)
    • 国際学会 / 招待講演
  • [学会発表] Advances in verified set and function calculi in Coq2023

    • 著者名/発表者名
      Pieter Collins, Sewon Park and Holger Thies
    • 学会等名
      Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2023)
    • 国際学会
  • [学会発表] Verifying iRRAM-like implementation of exact real computation2023

    • 著者名/発表者名
      Sewon Park and Holger Thies
    • 学会等名
      Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2023)
    • 国際学会
  • [学会発表] Towards verified implementation of iterative and interactive real-RAM2023

    • 著者名/発表者名
      Sewon Park and Holger Thies
    • 学会等名
      20th International Conference on Computability and Complexity in Analysis (CCA 2023)
    • 国際学会
  • [学会発表] Extending cAERN to spaces of subsets2023

    • 著者名/発表者名
      Michal Konecny, Sewon Park, Holger Thies
    • 学会等名
      29th International Conference on Types for Proofs and Programs (TYPES 2023)
    • 国際学会

URL: 

公開日: 2024-12-25  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi