2 papers
cs.LO2026
Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
Jackson Brough
Real numbers in constructive mathematics have always seemed to require compromises of one form or another. Classical proofs of Cauchy completeness require countable choice, Bishop'…
cs.PL2024
Target-Aware Implementation of Real Expressions
Brett Saiki, Jackson Brough, Jonas Regehr +5
New low-precision accelerators, vector instruction sets, and library functions make maximizing accuracy and performance of numerical code increasingly challenging. Two lines of wor…