Computable decision making on the reals and other spaces via partiality and nondeterminism

Benjamin Sherman, Luke Sciarappa, Adam Chlipala +1

Though many safety-critical software systems use floating point to represent real-world input and output, programmers usually have idealized versions in mind that compute with real…