乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T05:23:48Z","timestamp":1672377828249},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"1\/2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Commun. Comput. Algebra"],"published-print":{"date-parts":[[2010,7,29]]},"abstract":"Generating certified and efficient numerical codes requires information ranging from the mathematical level to the representation of numbers. Even though the mathematical semantics can be expressed using the content part of MathML, this language does not encompass the implementation on computers. Indeed various arithmetics may be involved, like floating-point or fixed-point, in fixed precision or arbitrary precision, and current tools do not handle all of these.<\/jats:p>\n Therefore we propose in this paper LEMA (Langage pour les Expressions Math'ematiques Annot'ees), a descriptive language based on MathML with additional expressiveness. LEMA will be used during the automatic generation of certified numerical codes. Such a generation process typically involves several steps, and LEMA would thus act as a glue to represent and store the information at every stage.<\/jats:p>\n First, we specify in the language the characteristics of the arithmetic as described in the IEEE 754 floatingpoint standard: formats, exceptions, rounding modes. This can be generalized to other arithmetics. Then, we use annotations to attach a specific arithmetic context to an expression tree. Finally, considering the evaluation of the expression in this context allows us to deduce several properties on the result, like being exact or being an exception. Other useful properties include numerical ranges and error bounds.<\/jats:p>","DOI":"10.1145\/1838599.1838622","type":"journal-article","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T13:15:22Z","timestamp":1280754922000},"page":"41-52","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["LEMA"],"prefix":"10.1145","volume":"44","author":[{"given":"Vincent","family":"Lef\u00e8vre","sequence":"first","affiliation":[{"name":"UMR 5668 CNRS - ENS de Lyon - INRIA - UCBL, Universit\u00e9 de Lyon"}]},{"given":"Philippe","family":"Th\u00e9veny","sequence":"additional","affiliation":[{"name":"UMR 5668 CNRS - ENS de Lyon - INRIA - UCBL, Universit\u00e9 de Lyon"}]},{"given":"Florent","family":"de Dinechin","sequence":"additional","affiliation":[{"name":"UMR 5668 CNRS - ENS de Lyon - INRIA - UCBL, Universit\u00e9 de Lyon"}]},{"given":"Claude-Pierre","family":"Jeannerod","sequence":"additional","affiliation":[{"name":"UMR 5668 CNRS - ENS de Lyon - INRIA - UCBL, Universit\u00e9 de Lyon"}]},{"given":"Christophe","family":"Mouilleron","sequence":"additional","affiliation":[{"name":"UMR 5668 CNRS - ENS de Lyon - INRIA - UCBL, Universit\u00e9 de Lyon"}]},{"given":"David","family":"Pfannholzer","sequence":"additional","affiliation":[{"name":"UMR 5668 CNRS - ENS de Lyon - INRIA - UCBL, Universit\u00e9 de Lyon"}]},{"given":"Nathalie","family":"Revol","sequence":"additional","affiliation":[{"name":"UMR 5668 CNRS - ENS de Lyon - INRIA - UCBL, Universit\u00e9 de Lyon"}]}],"member":"320","published-online":{"date-parts":[[2010,7,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511921698","volume-title":"Modern Computer Arithmetic","author":"Brent R.","year":"2010","unstructured":"R. Brent and P. Zimmermann . Modern Computer Arithmetic . Mar. 2010 . URL http:\/\/www.loria.fr\/~zimmerma\/mca\/mca-cup-0.5.1.pdf. Version 0.5.1. R. Brent and P. Zimmermann. Modern Computer Arithmetic. Mar. 2010. URL http:\/\/www.loria.fr\/~zimmerma\/mca\/mca-cup-0.5.1.pdf. Version 0.5.1."},{"key":"e_1_2_1_2_1","first-page":"9","volume-title":"VI Simp\u00f3sio Brasileiro de Computa\u00e7\u00e3o Gr\u00e1fica e Processamento de Imagens (SIBGRAPI'93)","author":"Comba J. L. D.","year":"1993","unstructured":"J. L. D. Comba and J. Stolfi . Affine arithmetic and its applications to computer graphics . In VI Simp\u00f3sio Brasileiro de Computa\u00e7\u00e3o Gr\u00e1fica e Processamento de Imagens (SIBGRAPI'93) , pages 9 -- 18 , Oct. 1993 . J. L. D. Comba and J. Stolfi. Affine arithmetic and its applications to computer graphics. In VI Simp\u00f3sio Brasileiro de Computa\u00e7\u00e3o Gr\u00e1fica e Processamento de Imagens (SIBGRAPI'93), pages 9--18, Oct. 1993."},{"key":"e_1_2_1_3_1","unstructured":"CRlibm. CRlibm (Correctly Rounded mathematical library). URL http:\/\/lipforge.ens-lyon.fr\/www\/crlibm\/. CRlibm. CRlibm (Correctly Rounded mathematical library). URL http:\/\/lipforge.ens-lyon.fr\/www\/crlibm\/."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1644001.1644003"},{"key":"e_1_2_1_5_1","volume-title":"OpenMath Content Dictionary: bigfloat1","author":"Davenport J.","year":"1999","unstructured":"J. Davenport . OpenMath Content Dictionary: bigfloat1 , 1999 . URL http:\/\/www.openmath.org\/cd\/bigfloat1.ocd. J. Davenport. OpenMath Content Dictionary: bigfloat1, 1999. URL http:\/\/www.openmath.org\/cd\/bigfloat1.ocd."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1141277.1141584"},{"key":"e_1_2_1_7_1","volume-title":"Rio de Janeiro","author":"de Figueiredo L. H.","year":"1997","unstructured":"L. H. de Figueiredo and J. Stolfi . Self-Validated Numerical Methods and Applications. Brazilian Mathematics Colloquium monographs. IMPA\/CNPq , Rio de Janeiro , Brazil , 1997 . L. H. de Figueiredo and J. Stolfi. Self-Validated Numerical Methods and Applications. Brazilian Mathematics Colloquium monographs. IMPA\/CNPq, Rio de Janeiro, Brazil, 1997."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11515-8_26"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01397083"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04570-7_6"},{"key":"e_1_2_1_12_1","first-page":"173","volume-title":"CAV","author":"Filli\u00e2tre J.-C.","year":"2007","unstructured":"J.-C. Filli\u00e2tre and C. March\u00e9 . The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification . In CAV , pages 173 -- 177 , Berlin, Germany , 2007 . J.-C. Filli\u00e2tre and C. March\u00e9. The Why\/Krakatoa\/Caduceus Platform for Deductive Program Verification. In CAV, pages 173--177, Berlin, Germany, 2007."},{"key":"e_1_2_1_13_1","unstructured":"FLIP. FLIP (Floating-point Library for Integer Processors). URL http:\/\/flip.gforge.inria.fr\/. FLIP. FLIP (Floating-point Library for Integer Processors). URL http:\/\/flip.gforge.inria.fr\/."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1236463.1236468"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03034-5_18"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_3"},{"key":"e_1_2_1_17_1","first-page":"978","article-title":"IEEE Standard for Floating-Point Arithmetic","volume":"754","author":"IEEE Computer Society","year":"2008","unstructured":"IEEE Computer Society . IEEE Standard for Floating-Point Arithmetic . IEEE Standard 754-2008 , Aug. 2008 . ISBN 978 - 970 -7381-5752-8. Available at http:\/\/ieeexplore.ieee.org\/servlet\/opac?punumber=4610933. IEEE Computer Society. IEEE Standard for Floating-Point Arithmetic. IEEE Standard 754-2008, Aug. 2008. ISBN 978-0-7381-5752-8. Available at http:\/\/ieeexplore.ieee.org\/servlet\/opac?punumber=4610933.","journal-title":"IEEE Standard"},{"key":"e_1_2_1_18_1","volume-title":"Programming Languages -- C. ISO\/IEC Standard 9899:1999","author":"International Organization for Standardization.","year":"1999","unstructured":"International Organization for Standardization. Programming Languages -- C. ISO\/IEC Standard 9899:1999 , Geneva, Switzerland , Dec. 1999 . International Organization for Standardization. Programming Languages -- C. ISO\/IEC Standard 9899:1999, Geneva, Switzerland, Dec. 1999."},{"key":"e_1_2_1_20_1","unstructured":"MathML. Mathematical markup language (MathML) version 3.0. URL http:\/\/www.w3.org\/TR\/2009\/CR-MathML3-20091215\/. MathML. Mathematical markup language (MathML) version 3.0. URL http:\/\/www.w3.org\/TR\/2009\/CR-MathML3-20091215\/."},{"key":"e_1_2_1_21_1","unstructured":"G. Melquiond. User's Guide for Gappa. URL http:\/\/gappa.gforge.inria.fr\/doc\/index.html. G. Melquiond. User's Guide for Gappa. URL http:\/\/gappa.gforge.inria.fr\/doc\/index.html."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01975722"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1823389"},{"key":"e_1_2_1_25_1","first-page":"3023","author":"Network Working Group","year":"2001","unstructured":"Network Working Group . XML Media Types , 2001 . RFC 3023 . Network Working Group. XML Media Types, 2001. RFC 3023.","journal-title":"XML Media Types"},{"key":"e_1_2_1_26_1","volume-title":"The openmath standard, version 2.0","year":"2004","unstructured":"OpenMath2. The openmath standard, version 2.0 , 2004 . URL http:\/\/www.openmath.org\/standard\/om20-2004-06-30\/omstd20html-0.xml. OpenMath2. The openmath standard, version 2.0, 2004. URL http:\/\/www.openmath.org\/standard\/om20-2004-06-30\/omstd20html-0.xml."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2004.840306"},{"key":"e_1_2_1_28_1","volume-title":"Encyclopedia of Parallel Computing","author":"P\u00fcschel M.","year":"2011","unstructured":"M. P\u00fcschel , F. Franchetti , and Y. Voronenko . Encyclopedia of Parallel Computing , chapter Spiral. Springer , 2011 . M. P\u00fcschel, F. Franchetti, and Y. Voronenko. Encyclopedia of Parallel Computing, chapter Spiral. Springer, 2011."},{"key":"e_1_2_1_29_1","series-title":"Lecture Notes in Computer Science","first-page":"295","volume-title":"Novel Approaches to Verification","author":"Putot S.","year":"2004","unstructured":"S. Putot , E. Goubault , and M. Martel . Static analysis-based validation of floating-point computations . In Novel Approaches to Verification , volume 2991 of Lecture Notes in Computer Science , pages 295 -- 312 , 2004 . S. Putot, E. Goubault, and M. Martel. Static analysis-based validation of floating-point computations. In Novel Approaches to Verification, volume 2991 of Lecture Notes in Computer Science, pages 295--312, 2004."}],"container-title":["ACM Communications in Computer Algebra"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1838599.1838622","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T19:41:10Z","timestamp":1672342870000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1838599.1838622"}},"subtitle":["towards a language for reliable arithmetic"],"short-title":[],"issued":{"date-parts":[[2010,7,29]]},"references-count":26,"journal-issue":{"issue":"1\/2","published-print":{"date-parts":[[2010,7,29]]}},"alternative-id":["10.1145\/1838599.1838622"],"URL":"https:\/\/doi.org\/10.1145\/1838599.1838622","relation":{},"ISSN":["1932-2240"],"issn-type":[{"value":"1932-2240","type":"print"}],"subject":[],"published":{"date-parts":[[2010,7,29]]},"assertion":[{"value":"2010-07-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}