A formally verified floating-point implementation of the compact position reporting algorithm
scientific article; zbMATH DE number 7343222