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]. |