diff --git a/metadata/entries/IEEE_Floating_Point.toml b/metadata/entries/IEEE_Floating_Point.toml --- a/metadata/entries/IEEE_Floating_Point.toml +++ b/metadata/entries/IEEE_Floating_Point.toml @@ -1,53 +1,51 @@ title = "A Formal Model of IEEE Floating Point Arithmetic" date = 2013-07-27 topics = [ "Computer science/Data structures", ] abstract = "This development provides a formal model of IEEE-754 floating-point arithmetic. This formalization, including formal specification of the standard and proofs of important properties of floating-point arithmetic, forms the foundation for verifying programs with floating-point computation. There is also a code generation setup for floats so that we can execute programs using this formalization in functional programming languages." license = "bsd" note = "" [authors] [authors.yu] email = "yu_email" [contributors] [contributors.hellauer] email = "hellauer_email" [contributors.immler] homepage = "immler_homepage" [contributors.weber] email = "weber_email" [notify] paulson = "paulson_email" immler = "immler_email" weber = "weber_email" [history] 2017-09-25 = """ Added conversions from and to software floating point numbers (by Fabian Hellauer and Fabian Immler).
""" 2018-02-05 = """ 'Modernized' representation following the formalization in HOL4: former \"float_format\" and predicate \"is_valid\" is now encoded in a type \"('e, 'f) float\" where 'e and 'f encode the size of exponent and fraction.
""" 2023-05-10 = """ Added the IEEE rounding mode \"roundNearestTiesToAway\".
""" 2023-05-22 = """ Added a model of floating-point arithmetic with a single NaN value.
-""" -2023-05-22 = """ Added a translation of floating-point arithmetic into SMT-LIB.
""" [extra] [related]