2 citations · 4 across the 5 of their papers we have counts for
6 papers
Formal verification of tilt estimation using the Rocq prover
Reynald Affeldt, Lynda Bentoucha, Yoshihiro Ishiguro +1
The safe operation of a humanoid robot critically relies on accurate estimation of its vertical orientation, or ``tilt''. This requires a variety of mathematical tools, including t…
Algorithmic Cost in "Exact Real Computation"
Jihoon Hyun, Holger Thies, Martin Ziegler
Turing completeness of a programming language or system characterizes its expressive power; and the strong Church-Turing hypo-/thesis refines such from qualitative to polynomial-ti…
Formalizing Hyperspaces and Operations on Subsets of Polish Spaces over Abstract Exact Real Numbers
Michal Konečný, Sewon Park, Holger Thies
Building on our prior work on axiomatization of exact real computation by formalizing nondeterministic first-order partial computations over real and complex numbers in a construct…
Extracting efficient exact real number computation from proofs in constructive type theory
Michal Konečný, Sewon Park, Holger Thies
Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When prov…
Continuous and monotone machines
Michal Konečný, Florian Steinberg, Holger Thies
We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The r…
Computable analysis and notions of continuity in Coq
Florian Steinberg, Laurent Thery, Holger Thies
We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of oper…