2 citations · 2 across the 3 of their papers we have counts for
5 papers
Auto-active Verification of Floating-point Programs via Nonlinear Real Provers
Junaid Rasheed, Michal Konečný
We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying programs against tight error bo…
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…
Implementing evaluation strategies for continuous real functions
Michal Konečný, Eike Neumann
We give a technical overview of our exact-real implementation of various representations of the space of continuous unary real functions over the unit domain and a family of associ…
Representations and evaluation strategies for feasibly approximable functions
Michal Konečný, Eike Neumann
A famous result due to Ko and Friedman (1982) asserts that the problems of integration and maximisation of a univariate real function are computationally hard in a well-defined sen…