Interpretation of IEEE-854 Floating-Point Standard and Definition in the HOL System
A Carreno Victor · NASA Technical Reports Server (NASA) · 1995
The ANSI/IEEE Standard 854-1987 for floating-point arithmetic is interpreted by converting the lexical descriptions in the standard into mathematical conditional descriptions organized in tables. The standard is represented in higher-order logic within the framework of the HOL system. The paper is divided in two parts with the first part the interpretation and the second part the description in HOL.