Marco Benini, Dirk Nowotka, and Carl Pulley
Computer Arithmetic: Logic, Calculation, and Rewriting


Frontiers of Combining Systems, Amsterdam 1998

This paper describes the concepts behind the Computer Arithmetic Toolkit (CAT) for the Isabelle/HOL system written by the authors.

Full paper: [ps - 188 KB] [ps.gz - 75 KB] [pdf - 138 KB].