Final exam - Lazy Exact Real Arithmetic Using Floating Point Operations

June 3, 2019 - 1:00pm
2520C UCC

PhD Candidate: Ryan McCleeary


Exact real arithmetic systems can specify any amount of precision on the output of their computations. They are used in a wide variety of applications when a high degree of precision is necessary. Some of these applications include: differential equation solvers, linear equation solvers, large scale mathematical models, and SMT solvers.

This dissertation proposes a new exact real arithmetic system which uses lazy lists of floating point numbers to represent the real numbers. It proposes algorithms for basic arithmetic computations on these structures and proves their correctness. This proposed system has the advantage of algorithms which can be supported by modern floating point hardware, while still being lazy and exact.

Advisor: Aaron Stump