{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T11:53:28Z","timestamp":1777636408042,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642226724","type":"print"},{"value":"9783642226731","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22673-1_3","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T07:49:15Z","timestamp":1310543355000},"page":"30-44","source":"Crossref","is-referenced-by-count":8,"title":["Incidence Simplicial Matrices Formalized in Coq\/SSReflect"],"prefix":"10.1007","author":[{"given":"J\u00f3nathan","family":"Heras","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mar\u00eda","family":"Poza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maxime","family":"D\u00e9n\u00e8s","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurence","family":"Rideau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Mathematical components team homepage, http:\/\/www.msr-inria.inria.fr\/Projects\/math-components"},{"issue":"4","key":"3_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. Journal of Automated Reasoning\u00a040(4), 271\u2013292 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0166-218X(02)00221-4","volume":"125","author":"R. Ayala","year":"2003","unstructured":"Ayala, R., Dom\u00ednguez, E., Franc\u00e9s, A., Quintero, A.: Homotopy in digital spaces. Discrete Applied Mathematics\u00a0125, 3\u201324 (2003)","journal-title":"Discrete Applied Mathematics"},{"key":"3_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art: the Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: the Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"key":"3_CR6","unstructured":"Coq development team: The Coq Proof Assistant Reference Manual, version 8.3. Tech. rep. (2010)"},{"key":"3_CR7","series-title":"Contemporary Mathematics","first-page":"143","volume-title":"Advances in Discrete and Computational Geometry","author":"T.K. Dey","year":"1999","unstructured":"Dey, T.K., Edelsbrunner, H., Guha, S.: Computational topology. In: Advances in Discrete and Computational Geometry. Contemporary Mathematics, pp. 143\u2013190. AMS, Providence (1999)"},{"key":"3_CR8","unstructured":"Dom\u00ednguez, C., Rubio, J.: Effective Homology of Bicomplexes, formalized in Coq. To appear in Theoretical Computer Science"},{"key":"3_CR9","unstructured":"Dousson, X., Sergeraert, F., Siret, Y.: The Kenzo program. Institut Fourier, Grenoble (1998), http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo"},{"key":"3_CR10","unstructured":"Gonthier, G.: Formal proof - The Four-Color Theorem. Notices of the American Mathematical Society, vol.\u00a055 (2008)"},{"key":"3_CR11","unstructured":"Gonthier, G., Mahboubi, A.: A Small Scale Reflection Extension for the Coq system. Tech. rep., Microsoft Research INRIA (2009), http:\/\/hal.inria.fr\/inria-00258384"},{"key":"3_CR12","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":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/11555964_18","volume-title":"Computer Algebra in Scientific Computing","author":"R. Gonzalez-Diaz","year":"2005","unstructured":"Gonzalez-Diaz, R., Medrano, B., Real, P., Sanchez-Pelaez, J.: Algebraic Topological Analysis of Time-Sequence of Digital Images. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2005. LNCS, vol.\u00a03718, pp. 208\u2013219. Springer, Heidelberg (2005)"},{"issue":"2-3","key":"3_CR14","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/j.dam.2004.09.014","volume":"147","author":"R. Gonzalez-Diaz","year":"2005","unstructured":"Gonzalez-Diaz, R., Real, P.: On the Cohomology of 3D Digital Images. Discrete Applied Math.\u00a0147(2-3), 245\u2013263 (2005)","journal-title":"Discrete Applied Math."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Heras, J., Poza, M., D\u00e9n\u00e8s, M., Rideau, L.: Incidence simplicial matrices formalized in SSReflect (2010), http:\/\/www.unirioja.es\/cu\/joheras\/ismfissr\/","DOI":"10.1007\/978-3-642-22673-1_3"},{"key":"3_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"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1126\/science.301.5634.756","volume":"8","author":"D. Mackenzie","year":"2003","unstructured":"Mackenzie, D.: Topologists and Roboticists Explore and Inchoate World. Science\u00a08, 756 (2003)","journal-title":"Science"},{"key":"3_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-62029-4","volume-title":"Homology","author":"S. MacLane","year":"1963","unstructured":"MacLane, S.: Homology. Springer, Heidelberg (1963)"},{"issue":"4","key":"3_CR19","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/s00454-003-2845-5","volume":"30","author":"D. Orden","year":"2003","unstructured":"Orden, D., Santos, F.: Asymptotically efficient triangulations of the d-cube. Discrete and Computational Geometry\u00a030(4), 509\u2013528 (2003)","journal-title":"Discrete and Computational Geometry"},{"key":"3_CR20","unstructured":"Rubio, J., Sergeraert, F.: Constructive Homological Algebra and Applications, Lecture Notes Summer School on Mathematics, Algorithms, and Proofs. University of Genova (2006), http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Papers\/Genova-Lecture-Notes.pdf"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/978-3-540-39903-2_85","volume-title":"Medical Image Computing and Computer-Assisted Intervention - MICCAI 2003","author":"F. S\u00e9gonne","year":"2003","unstructured":"S\u00e9gonne, F., Grimson, E., Fischl, B.: Topological Correction of Subcortical Segmentation. In: Ellis, R.E., Peters, T.M. (eds.) MICCAI 2003. LNCS, vol.\u00a02879, pp. 695\u2013702. Springer, Heidelberg (2003)"},{"key":"3_CR22","unstructured":"Veblen, O.: Analysis Situs. AMS Coll. Publ. (1931)"},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/0097-3165(89)90053-8","volume":"50","author":"J. Wood","year":"1989","unstructured":"Wood, J.: Spinor groups and algebraic coding theory. Journal of Combinatorial Theory\u00a050, 277\u2013313 (1989)","journal-title":"Journal of Combinatorial Theory"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22673-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T19:19:26Z","timestamp":1560367166000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}