Go to the corresponding LIPIcs Volume Portal 
Bertholon, Guillaume ; MartinDorel, Érik ; Roux, Pierre
pdfformat: 

@InProceedings{bertholon_et_al:LIPIcs:2019:11062, author = {Guillaume Bertholon and {\'E}rik MartinDorel and Pierre Roux}, title = {{Primitive Floats in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {7:17:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {9783959771221}, ISSN = {18688969}, year = {2019}, volume = {141}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik}, address = {Dagstuhl, Germany}, URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11062}, URN = {urn:nbn:de:0030drops110629}, doi = {10.4230/LIPIcs.ITP.2019.7}, annote = {Keywords: Coq formal proofs, floatingpoint arithmetic, reflexive tactics, Cholesky decomposition} }
Keywords:  Coq formal proofs, floatingpoint arithmetic, reflexive tactics, Cholesky decomposition  
Seminar:  10th International Conference on Interactive Theorem Proving (ITP 2019)  
Issue Date:  2019  
Date of publication:  06.09.2019 