Details About PVS Float Library

%------------------------------------------------------------------------
% Formalization of Floating Point numbers in PVS
%  
% The hardware level model was developed by Paul Miner (NASA LaRC). 
%   P. Miner, Defining the IEEE-854 floating-point standard in PVS, 
%   NASA/TM-95-110167, NASA Langley Research Center, 1995.
%   http://techreports.larc.nasa.gov/ltrs/dublincore/1995/NASA-95-tm110167.html
%
% The high level model was developed by Sylvie Boldo (ENS-Lyon) while 
% visiting NIA. 
%   S. Boldo, Preuves formelles en arithmetiques a virgule flottante, 
%   PhD. Thesis, Ecole Normale Superieure de Lyon, 2004.
%   http://www.ens-lyon.fr/LIP/Pub/Rapports/PhD/PhD2004/PhD2004-05.pdf
%
%------------------------------------------------------------------------

  % High-level model (SB)
            float, axpy, 
            
  % Hardware-level (PM)
            IEEE_854, IEEE_854_defs, infinity_arithmetic,
            comparison1, NaN_ops, arithmetic_ops, IEEE_854_remainder,
            IEEE_854_fp_int, real_to_fp, over_under, 
            IEEE_854_values, round, fp_round_aux,
            sum_lemmas, enumerated_type_defs, sum_hack,
            
  % Equivalence between the two models (SB)
            IEEE_link