{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:21:21Z","timestamp":1750306881508,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":13,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,6,26]],"date-time":"2013-06-26T00:00:00Z","timestamp":1372204800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,6,26]]},"DOI":"10.1145\/2465506.2465515","type":"proceedings-article","created":{"date-parts":[[2013,6,25]],"date-time":"2013-06-25T19:13:21Z","timestamp":1372187601000},"page":"243-250","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Certified symbolic manipulation"],"prefix":"10.1145","author":[{"given":"Laureano","family":"Lamb\u00e1n","sequence":"first","affiliation":[{"name":"University of La Rioja, La Rioja, Spain"}]},{"given":"Francisco J.","family":"Mart\u00edn-Mateos","sequence":"additional","affiliation":[{"name":"University of Seville, Seville, Spain"}]},{"given":"Julio","family":"Rubio","sequence":"additional","affiliation":[{"name":"University of La Rioja, La Rioja, Spain"}]},{"given":"Jos\u00e9-Luis","family":"Ruiz-Reina","sequence":"additional","affiliation":[{"name":"University of Seville, Seville, Spain"}]}],"member":"320","published-online":{"date-parts":[[2013,6,26]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings ACL2 Workshop 2007","author":"Andr\u00e9s M.","year":"2007","unstructured":"M. Andr\u00e9s , L. Lamb\u00e1n , J. Rubio , and J.-L. Ruiz-Reina . Formalizing Simplicial Topology in ACL2 . Proceedings ACL2 Workshop 2007 , 34--39, 2007 . M. Andr\u00e9s, L. Lamb\u00e1n, J. Rubio, and J.-L. Ruiz-Reina. Formalizing Simplicial Topology in ACL2. Proceedings ACL2 Workshop 2007, 34--39, 2007."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9094-x"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00454-007-9042-x"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.11.016"},{"key":"e_1_3_2_1_5_1","volume-title":"Institut Fourier","author":"Dousson X.","year":"1999","unstructured":"X. Dousson , F. Sergeraert , and Y. Siret . The Kenzo program , Institut Fourier , Grenoble , 1999 .\\ http:\/\/www-fourier.ujf-grenoble.fr\/\\ sergerar \/Kenzo\/ X. Dousson, F. Sergeraert, and Y. Siret. The Kenzo program, Institut Fourier, Grenoble, 1999.\\ http:\/\/www-fourier.ujf-grenoble.fr\/\\ sergerar \/Kenzo\/"},{"key":"e_1_3_2_1_6_1","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann M.","year":"2010","unstructured":"M. Kaufmann , P. Manolios , and J S. Moore . Computer-Aided Reasoning: An Approach . Kluwer , 2010 . M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: An Approach. Kluwer, 2010."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-011-9274-6"},{"key":"e_1_3_2_1_8_1","volume-title":"Formalization of the Eilenberg-Zilber Theorem","author":"Lamb\u00e1n L.","year":"2012","unstructured":"L. Lamb\u00e1n , F.J. Mart\u0131n-Mateos , J. Rubio , and J.-L. Ruiz-Reina . Formalization of the Eilenberg-Zilber Theorem , 2012 .\\ http:\/\/www.glc.us.es\/fmartin\/acl2\/eztheorem L. Lamb\u00e1n, F.J. Mart\u0131n-Mateos, J. Rubio, and J.-L. Ruiz-Reina. Formalization of the Eilenberg-Zilber Theorem, 2012.\\ http:\/\/www.glc.us.es\/fmartin\/acl2\/eztheorem"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02614-0_13"},{"key":"e_1_3_2_1_10_1","volume-title":"Simplicial objects in Algebraic Topology","author":"May J. P.","year":"1967","unstructured":"J. P. May . Simplicial objects in Algebraic Topology . Van Nostrand , 1967 . J. P. May. Simplicial objects in Algebraic Topology. Van Nostrand, 1967."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2000.v2.n1.a5"},{"key":"e_1_3_2_1_13_1","volume-title":"Homotopy groups of suspended classifying spaces: an experimental approach. To appear in Mathematics of Computation","author":"Romero A.","year":"2013","unstructured":"A. Romero , and J. Rubio . Homotopy groups of suspended classifying spaces: an experimental approach. To appear in Mathematics of Computation , 2013 . A. Romero, and J. Rubio. Homotopy groups of suspended classifying spaces: an experimental approach. To appear in Mathematics of Computation, 2013."},{"key":"e_1_3_2_1_14_1","volume-title":"Th\u00e8se","author":"Rubio J.","year":"1991","unstructured":"J. Rubio . Homologie effective des espaces de lacets it\u00e9r\u00e9s : un logiciel . Th\u00e8se , Institut Fourier , 1991 .\\ http:\/\/dialnet.unirioja.es\/servlet \/tesis?codigo=1331 J. Rubio. Homologie effective des espaces de lacets it\u00e9r\u00e9s : un logiciel. Th\u00e8se, Institut Fourier, 1991.\\ http:\/\/dialnet.unirioja.es\/servlet \/tesis?codigo=1331"}],"event":{"name":"ISSAC'13: International Symposium on Symbolic and Algebraic Computation","sponsor":["SIGSAM ACM Special Interest Group on Symbolic and Algebraic Manipulation"],"location":"Boston Maine USA","acronym":"ISSAC'13"},"container-title":["Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2465506.2465515","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2465506.2465515","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:35Z","timestamp":1750234715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2465506.2465515"}},"subtitle":["bivariate simplicial polynomials"],"short-title":[],"issued":{"date-parts":[[2013,6,26]]},"references-count":13,"alternative-id":["10.1145\/2465506.2465515","10.1145\/2465506"],"URL":"https:\/\/doi.org\/10.1145\/2465506.2465515","relation":{},"subject":[],"published":{"date-parts":[[2013,6,26]]},"assertion":[{"value":"2013-06-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}