Combining Coq and Gappa for Certifying Floating-Point Programs

Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. In Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, Stephen M. Watt, editors, Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings. Volume 5625 of Lecture Notes in Computer Science, pages 59-74, Springer, 2009. [doi]

References

No references recorded for this publication.

Cited by

No citations of this publication recorded.