http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
verifying floating-point algorithms with the Coq system
1 online resource (xx, 306 pages): illustrations, text file, PDF.