Verified exact computation over continuous higher types

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

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.