proof.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -ob temp/proof.bib -c 'keywords : "formal proof"' metalibm.bib}}
@article{LIP64851,
  author = {Chevillard, Sylvain and Joldes, Mioara and Harrison, John and Lauter, Christoph},
  month = apr,
  title = {Efficient and accurate computation of upper bounds of approximation errors},
  journal = {Theoretical Computer Science},
  volume = {412},
  number = {16},
  year = {2011},
  pages = {1523-1543},
  url = {http://dl.acm.org/citation.cfm?id=1945130},
  doi = {http://dx.doi.org/10.1016/j.tcs.2010.11.052},
  keywords = {tools, approximation, formal proof, multiple precision}
}
@inproceedings{harrison-fmcad2000,
  author = {John Harrison},
  title = {Formal verification of floating point
        trigonometric functions},
  booktitle = {Formal Methods in Computer-Aided Design:
        Third International Conference {FMCAD} 2000},
  publisher = {Springer-Verlag},
  pages = {217--233},
  series = {Lecture Notes in Computer Science},
  volume = 1954,
  year = 2000,
  keywords = {formal proof, sin, cos}
}
@inproceedings{harrison97-exp,
  author = {John Harrison},
  title = {Floating Point Verification in {HOL} Light: The Exponential Function},
  booktitle = {Algebraic Methodology and Software Technology},
  pages = {246-260},
  year = {1997},
  url = {citeseer.ist.psu.edu/harrison97floating.html},
  keywords = {formal proof, exp}
}
@book{Knuth97,
  author = {Donald Knuth},
  year = 1997,
  title = {The Art of Computer Programming, vol.2: Seminumerical Algorithms},
  edition = {3rd},
  publisher = {Addison Wesley},
  keywords = {multiple precision, formal proof, division, textbook}
}
@article{DinechinLauterMelquiond2011:TC,
  author = {de Dinechin, Florent and Lauter, Christoph and Melquiond, Guillaume},
  doi = {10.1109/TC.2010.128},
  title = {Certifying the floating-point implementation of an elementary function using {G}appa},
  journal = {IEEE Transactions on Computers},
  publisher = {IEEE},
  pages = {242--253},
  year = 2011,
  month = feb,
  volume = 60,
  number = 2,
  url = {http://hal.inria.fr/inria-00533968/en},
  pdf = {http://perso.ens-lyon.fr/florent.de.dinechin/recherche/publis/2011-TC-ElemFun-Gappa.pdf},
  keywords = {formal proofs}
}
@inproceedings{BoldoMelquiond2011,
  author = {S. Boldo and G. Melquiond},
  booktitle = {ARITH 20},
  pages = {243–252},
  title = {Flocq: A Unified Library for Proving Floating-point Algorithms in {C}oq},
  url = {http://www.lri.fr/~melquion/doc/11-arith20-article.pdf},
  year = {2011},
  keywords = {formal proof}
}

This file was generated by bibtex2html 1.98.