research
∙
07/02/2022
Auto-active Verification of Floating-point Programs via Nonlinear Real Provers
We give a process for verifying numerical programs against their functio...
share
research
∙
02/02/2022
Extracting efficient exact real number computation from proofs in constructive type theory
Exact real computation is an alternative to floating-point arithmetic wh...
research
∙
05/04/2020
Continuous and monotone machines
We investigate a variant of the fuel-based approach to modeling divergin...
research
∙
10/10/2019
Implementing evaluation strategies for continuous real functions
We give a technical overview of our exact-real implementation of various...
research
∙
10/10/2017