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,39 +1,53 @@
 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).<br>
 """
 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."""
+'e and 'f encode the size of exponent and fraction.<br>
+"""
+2023-05-10 = """
+Added the IEEE rounding mode \"roundNearestTiesToAway\".<br>
+"""
+2023-05-22 = """
+Added a model of floating-point arithmetic with a single NaN value.<br>
+"""
+2023-05-22 = """
+Added a translation of floating-point arithmetic into SMT-LIB.<br>
+"""
 
 [extra]
 
 [related]