@entry{mon-dar-17-aa, author = {R Monat and E Darulov{\'a}}, title = {Certificate Checking in Coq and HOL4 for Static Analyses of Mixed-Precision Floating-Point Arithmetic}, journal = {}, volume = {}, number = {}, pages = {}, year = 2017, month = , doi = {}, comment = {}, abstract = {}, url = {{\url{https://rmonat.fr/data/M2_report.pdf}}}, quotes = {... In Section 4, I describe another ongoing work, which is a formalization of affine arithmetic in Coq. Section 5 provides a brief related work. The conclusion of my report also describes ...} }