Verified exact computation over continuous higher types

验证了连续较高类型的精确计算

• 批准号: 22KF0198
• 负责人: 河村 彰星
• 金额: $ 1.47万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2023
• 资助国家: 日本
• 起止时间: 2023-03-08 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22KF0198/
• 关键词: exact real computation; program verification; higher-order Hoare logic; constructive type theory; formalized mathematics

An imperative language for exact real number computation with pure higher-order function construction is proposed. The design is inspired by the standard functions in C++. The language is further equipped with primitive operators for countable nondeterministic choices and nondeterministic limits to make the language’s function construction useful. The language’s denotational semantics is formalized based on computable analysis and domain theory using an unbounded powerdomain for countable nondeterminism. Sound Hoare-style proof rules for the two additional primitive operations are devised. As an example, an imperative program nondeterministically computing a root of a continuous real function, a constructive variant of the Intermediate Value Theorem, is given and proved correct.Coq-AERN is an axiomatic formalization of exact real number computation in a constructive type theory and Coq. The formalization is extended with function spaces, open subsets, closed subsets, compact subsets, and overt subsets. Similarly to the programming language counterpart, this formalization is extended with countable choices. Examples of drawing various subsets, including some fractals, in Euclidean spaces are given.

提出了一种用纯高阶函数构造的精确真实的实数计算的命令式语言。设计灵感来自C++中的标准函数。该语言还配备了用于可数非确定性选择和非确定性限制的原始运算符，以使该语言的函数构造有用。该语言的指称语义是形式化的基础上可计算分析和域理论使用无限的幂域可数不确定性。声音霍尔式证明规则的两个额外的原始操作的设计。作为一个例子，给出了一个非确定性地计算连续真实的函数的根的命令程序，并证明了其正确性.Coq-AERN是构造型理论和Coq中精确真实的数计算的公理化形式.形式化扩展的功能空间，开子集，闭子集，紧凑的子集，和公开的子集。与编程语言类似，这种形式化扩展了可数选择。给出了在欧氏空间中绘制各种子集，包括一些分形的例子。

项目成果

A type-theoretical interpretation of intuitionistic fixed point logic

直觉定点逻辑的类型论解释

• 发表时间: 2022
• 作者: Ulrich Berger;Sewon Park;Holger Thies and Hideki Tsuiki
• 通讯作者: Holger Thies and Hideki Tsuiki

From Coq Proofs to Efficient Certified Exact Real Computation

从 Coq 证明到高效的认证精确真实计算

• 发表时间: 2022
• 作者: Michal Konecny;Sewon Park;Holger Thies
• 通讯作者: Holger Thies

Certified exact real computation on hyperspaces

超空间上经过认证的精确真实计算

• 发表时间: 2022
• 作者: Michal Konecny;Sewon Park;Holger Thies
• 通讯作者: Holger Thies

Some steps toward program extraction in a type-theoretical interpretation of IFP

IFP 类型理论解释中程序提取的一些步骤

• 发表时间: 2022
• 作者: Ulrich Berger;Sewon Park;Holger Thies;Hideki Tsuiki
• 通讯作者: Hideki Tsuiki

Nondeterministic limits and certified exact real computation

不确定性限制和经过认证的精确实际计算

• 发表时间: 2022
• 作者: Michal Konecny;Sewon Park;Holger Thies
• 通讯作者: Holger Thies