{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:49:18Z","timestamp":1725558558334},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141270"},{"type":"electronic","value":"9783642141287"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_18","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T06:45:36Z","timestamp":1277793936000},"page":"204-218","source":"Crossref","is-referenced-by-count":2,"title":["Computing in Coq with Infinite Algebraic Data Structures"],"prefix":"10.1007","author":[{"given":"C\u00e9sar","family":"Dom\u00ednguez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julio","family":"Rubio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-73086-6_1","volume-title":"Towards Mechanized Mathematical Assistants","author":"M. Andr\u00e9s","year":"2007","unstructured":"Andr\u00e9s, M., Lamb\u00e1n, L., Rubio, J.: Executing in Common Lisp, Proving in ACL2. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 1\u201312. Springer, Heidelberg (2007)"},{"issue":"4","key":"18_CR2","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s10817-007-9094-x","volume":"40","author":"J. Aransay","year":"2008","unstructured":"Aransay, J., Ballarin, C., Rubio, J.: A Mechanized Proof of the Basic Perturbation Lemma. J. Autom. Reason.\u00a040(4), 271\u2013292 (2008)","journal-title":"J. Autom. Reason."},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s00165-009-0120-0","volume":"22","author":"J. Aransay","year":"2010","unstructured":"Aransay, J., Ballarin, C., Rubio, J.: Generating certified code from formal proofs: a case study in homological algebra. Form. Asp. Comput.\u00a022, 193\u2013213 (2010)","journal-title":"Form. Asp. Comput."},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/978-3-642-04772-5_27","volume-title":"EUROCAST 2009","author":"J. Aransay","year":"2009","unstructured":"Aransay, J., Dom\u00ednguez, C.: Modelling Differential Structures in Proof Assistants: The Graded Case. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2009. LNCS, vol.\u00a05717, pp. 203\u2013210. Springer, Heidelberg (2009)"},{"key":"18_CR5","volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. In: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S. Boutin","year":"1997","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg (1997)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming, SIGPLAN Notices, vol.\u00a035(9), pp. 268\u2013279 (2000)","DOI":"10.1145\/357766.351266"},{"key":"18_CR8","unstructured":"Coquand, T., Spiwack, A.: Constructively finite. In: Contribuciones cient\u00edficas en honor de Mirian Andr\u00e9s G\u00f3mez. Servicio de Publicaciones de la Universidad de La Rioja (2010)"},{"key":"18_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-540-73086-6_4","volume-title":"Towards Mechanized Mathematical Assistants","author":"T. Coquand","year":"2007","unstructured":"Coquand, T., Spiwack, A.: Towards Constructive Homological Algebra in Type Theory. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 40\u201354. Springer, Heidelberg (2007)"},{"key":"18_CR10","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1051\/ita:2007015","volume":"41","author":"C. Dom\u00ednguez","year":"2007","unstructured":"Dom\u00ednguez, C., Lamb\u00e1n, L., Rubio, J.: Object-Oriented Institutions to Specify Symbolic Computation Systems. Rairo. Theor. Inf. Appl.\u00a041, 191\u2013214 (2007)","journal-title":"Rairo. Theor. Inf. Appl."},{"key":"18_CR11","unstructured":"Dom\u00ednguez, C., Rubio, J.: Effective Homology of Bicomplexes, formalized in Coq, \n                    \n                      https:\/\/esus.unirioja.es\/psycotrip\/archivos_documentos\/EHBFC.pdf"},{"key":"18_CR12","volume-title":"The Kenzo Program","author":"X. Dousson","year":"1999","unstructured":"Dousson, X., Sergeraert, F., Siret, Y.: The Kenzo Program. Institut Fourier, Grenoble (1999), \n                    \n                      http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo\/"},{"issue":"4","key":"18_CR13","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1006\/jsco.2002.0552","volume":"34","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput.\u00a034(4), 271\u2013286 (2002)","journal-title":"J. Symb. Comput."},{"issue":"11","key":"18_CR14","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal Proof: The Four-Color Theorem. Notices of the AMS\u00a055(11), 1382\u20131393 (2008)","journal-title":"Notices of the AMS"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-74591-4_8","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Gonthier","year":"2007","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Th\u00e9ry, L.: A Modular Formalisation of Finite Group Theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 86\u2013101. Springer, Heidelberg (2007)"},{"key":"18_CR16","volume-title":"Basic Algebra II","author":"N. Jacobson","year":"1989","unstructured":"Jacobson, N.: Basic Algebra II, 2nd edn. W.H. Freeman and Company, New York (1989)","edition":"2"},{"issue":"3","key":"18_CR17","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s00200-003-0129-1","volume":"14","author":"L. Lamb\u00e1n","year":"2003","unstructured":"Lamb\u00e1n, L., Pascual, V., Rubio, J.: An Object-Oriented Interpretation of the EAT System. Appl. Algebra Eng. Commun. Comput.\u00a014(3), 187\u2013215 (2003)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"L. Letouzey","year":"2008","unstructured":"Letouzey, L.: Extraction in Coq: An Overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol.\u00a05028, pp. 359\u2013369. Springer, Heidelberg (2008)"},{"key":"18_CR19","unstructured":"LogiCal project. The Coq Proof Assistant (2010), \n                    \n                      http:\/\/coq.inria.fr\/"},{"issue":"1","key":"18_CR20","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1017\/S096012950600586X","volume":"17","author":"A. Mahboubi","year":"2007","unstructured":"Mahboubi, A.: Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. Comput. Sci.\u00a017(1), 99\u2013127 (2007)","journal-title":"Math. Struct. Comput. Sci."},{"key":"18_CR21","unstructured":"May, P.: Simplicial Objects in Algebraic Topology. Van Nostrand (1967)"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL: A proof assistant for higher order logic, LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"10","key":"18_CR23","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1080\/00207160512331323326","volume":"82","author":"J. Rubio","year":"2005","unstructured":"Rubio, J., Sergeraert, F.: Computing with locally effective matrices. Int. J. Comput. Math.\u00a082(10), 1177\u20131189 (2005)","journal-title":"Int. J. Comput. Math."},{"key":"18_CR24","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1016\/S0007-4497(02)01119-3","volume":"126","author":"J. Rubio","year":"2002","unstructured":"Rubio, J., Sergeraert, F.: Constructive Algebraic Topology. Bull. Sci. math.\u00a0126, 389\u2013412 (2002)","journal-title":"Bull. Sci. math."},{"key":"18_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/aima.1994.1018","volume":"104","author":"F. Sergeraert","year":"1994","unstructured":"Sergeraert, F.: The computability problem in Algebraic Topology. Adv. Math.\u00a0104, 1\u201329 (1994)","journal-title":"Adv. Math."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:23:00Z","timestamp":1558279380000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}