• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2023 Fiscal Year Annual Research Report

Verified exact computation over continuous higher types

Research Project

Project/Area Number 22KF0198
Allocation TypeMulti-year Fund
Research InstitutionKyoto University

Principal Investigator

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

Co-Investigator(Kenkyū-buntansha) PARK SEWON  京都大学, 数理解析研究所, 外国人特別研究員
Project Period (FY) 2023-03-08 – 2024-03-31
Keywordsexact real computation / program verification / higher-order Hoare logic / constructive type theory / formalized mathematics
Outline of Annual Research Achievements

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.

  • Research Products

    (8 results)

All 2024 2023 Other

All Int'l Joint Research (1 results) Journal Article (2 results) (of which Int'l Joint Research: 1 results,  Peer Reviewed: 2 results,  Open Access: 1 results) Presentation (5 results) (of which Int'l Joint Research: 5 results,  Invited: 1 results)

  • [Int'l Joint Research] マーストリヒト大学(オランダ)

    • Country Name
      NETHERLANDS
    • Counterpart Institution
      マーストリヒト大学
  • [Journal Article] Formalizing hyperspaces for extracting efficient exact real computation2023

    • Author(s)
      Michal Konecny;, Sewon Park, and Holger Thies
    • Journal Title

      Leibniz International Proceedings in Informatics

      Volume: 272 Pages: 59

    • DOI

      10.4230/LIPIcs.MFCS.2023.59

    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Verified exact real computation with nondeterministic functions and limits2023

    • Author(s)
      Park Sewon
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 14292 Pages: 363~377

    • DOI

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

    • Peer Reviewed
  • [Presentation] Abstract data type for exact real numbers and verified computation2024

    • Author(s)
      Sewon Park
    • Organizer
      17th International Conference on Computability, Complexity and Randomness (CCR2024)
    • Int'l Joint Research / Invited
  • [Presentation] Advances in verified set and function calculi in Coq2023

    • Author(s)
      Pieter Collins, Sewon Park and Holger Thies
    • Organizer
      Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2023)
    • Int'l Joint Research
  • [Presentation] Verifying iRRAM-like implementation of exact real computation2023

    • Author(s)
      Sewon Park and Holger Thies
    • Organizer
      Continuity, Computability, Constructivity - From Logic to Algorithms (CCC 2023)
    • Int'l Joint Research
  • [Presentation] Towards verified implementation of iterative and interactive real-RAM2023

    • Author(s)
      Sewon Park and Holger Thies
    • Organizer
      20th International Conference on Computability and Complexity in Analysis (CCA 2023)
    • Int'l Joint Research
  • [Presentation] Extending cAERN to spaces of subsets2023

    • Author(s)
      Michal Konecny, Sewon Park, Holger Thies
    • Organizer
      29th International Conference on Types for Proofs and Programs (TYPES 2023)
    • Int'l Joint Research

URL: 

Published: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi