Computational complexity and practice of verified and efficient algorithms for dynamical systems

在类型论中精确实计算的形式化及其在Coq证明助手中的实现方面取得了很大进展。以往关于实数和复数的不确定性计算的形式化工作得到了扩展和统一。特别是在精确实际计算中的不确定性的形式化方面取得了进展，并提出了一个合理的多值极限算子的概念。该理论在Coq证明助手中实现，利用Coq的程序提取机制可以提取出精确实际计算的高效Haskell程序。作为一个非平凡的应用，我们提取了一个计算复平方根的不确定性程序。随着今年新冠肺炎相关边境限制的放松，国际联合研究可能会恢复。在英国阿斯顿大学的michael Konecny的访问期间，我们将上述形式化扩展到子集和函数的空间，这对微分方程有重要的应用，特别是关于可达性问题。在效率方面比较了处理子集的几种表示，并提取了用于生成子集绘图的认证程序，并显示其在运行时间方面表现良好。例子包括二维欧几里得空间中的分形。在将基于逻辑的证明系统IFP纳入我国类型理论工作方面也取得了进展。基于meta-coq框架，在Coq中开发了一个IFP风格证明系统和一个类似于IFP的无类型lambda演算提取程序。

Large progress has been made on the formalization of exact real computation in type theory and its implementation in the Coq proof assistant. Previous work on formalizing nondeterministic computation on real and complex numbers has been extended and unified. In particular, progress has been made on formalizing nondeterminism occuring in exact real computation and a sound notion of a multivalued limit operator was devised. The theory was implemented in the Coq proof assistant and using Coq's program extraction mechanism efficient Haskell programs for exact real computation can be extracted. As a non-trivial application we extract a nondeterministic program computing the complex square root.As Covid-19 related border restrictions loosened during this year, international joint research could be resumed. During a visit by Michal Konecny (Aston University, UK), we extended the aforementioned formalization to spaces of subsets and functions, which has important applications to differential equations, in particular regarding reachability questions.Several representations for dealing with subsets have been compared in terms of efficiency and certfied programs for generating drawings of subsets have been extracted and shown to behave well in terms of running time. Examples include fractals in two dimensional Euclidean space.Progress has also been made on integrating the logic based proof system IFP into our type theoretical work. A system for IFP style proofs in Coq and a new program extraction to untyped lambda calculus similar to IFP was developed based on the meta-coq framework.