{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:53:29Z","timestamp":1725515609216},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313738"},{"type":"electronic","value":"9783642313745"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_15","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T09:00:57Z","timestamp":1340614857000},"page":"216-230","source":"Crossref","is-referenced-by-count":3,"title":["Verifying an Algorithm Computing Discrete Vector Fields for Digital Imaging"],"prefix":"10.1007","author":[{"given":"J\u00f3nathan","family":"Heras","sequence":"first","affiliation":[]},{"given":"Mar\u00eda","family":"Poza","sequence":"additional","affiliation":[]},{"given":"Julio","family":"Rubio","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Mathematical components team homepage, \n                    \n                      http:\/\/www.msr-inria.inria.fr\/Projects\/math-components"},{"issue":"4","key":"15_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":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45685-6_4","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Barthe","year":"2002","unstructured":"Barthe, G., Courtieu, P.: Efficient Reasoning about Executable Specifications in Coq. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 31\u201346. Springer, Heidelberg (2002)"},{"key":"15_CR4","unstructured":"Bear, M., Connors, B., Paradiso, M.: Neuroscience: Exploring the Brain. Lippincott Williams & Wilkins (2006)"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In: ACM SIGPLAN Notices, pp. 268\u2013279. ACM Press (2000)","DOI":"10.1145\/357766.351266"},{"key":"15_CR6","unstructured":"Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination (2011), \n                    \n                      http:\/\/hal.inria.fr\/inria-00593738"},{"key":"15_CR7","unstructured":"Coq development team. The Coq Proof Assistant, version 8.3. Technical report (2010)"},{"issue":"8","key":"15_CR8","doi-asserted-by":"publisher","first-page":"2721","DOI":"10.1523\/JNEUROSCI.4477-10.2011","volume":"31","author":"G. Cuesto","year":"2011","unstructured":"Cuesto, G., et al.: Phosphoinositide-3-Kinase Activation Controls Synaptogenesis and Spinogenesis in Hippocampal Neurons. The Journal of Neuroscience\u00a031(8), 2721\u20132733 (2011)","journal-title":"The Journal of Neuroscience"},{"key":"15_CR9","doi-asserted-by":"publisher","first-page":"962","DOI":"10.1016\/j.tcs.2010.11.016","volume":"412","author":"C. Dom\u00ednguez","year":"2011","unstructured":"Dom\u00ednguez, C., Rubio, J.: Effective Homology of Bicomplexes, formalized in Coq. Theoretical Computer Science\u00a0412, 962\u2013970 (2011)","journal-title":"Theoretical Computer Science"},{"key":"15_CR10","unstructured":"Dousson, X., Rubio, J., Sergeraert, F., Siret, Y.: The Kenzo program. Institut Fourier, Grenoble (1998), \n                    \n                      http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo\/"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1006\/aima.1997.1650","volume":"134","author":"R. Forman","year":"1998","unstructured":"Forman, R.: Morse theory for cell complexes. Advances in Mathematics\u00a0134, 90\u2013145 (1998)","journal-title":"Advances in Mathematics"},{"key":"15_CR12","unstructured":"Gonthier, G.: Formal proof - The Four-Color Theorem, vol.\u00a055. Notices of the American Mathematical Society (2008)"},{"issue":"2","key":"15_CR13","first-page":"95","volume":"3","author":"G. Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. Journal of Formal Reasoning\u00a03(2), 95\u2013152 (2010)","journal-title":"Journal of Formal Reasoning"},{"key":"15_CR14","unstructured":"Graham, P.: ANSI Common Lisp. Prentice Hall (1996)"},{"key":"15_CR15","unstructured":"Heras, J., D\u00e9n\u00e8s, M., Mata, G., M\u00f6rtberg, A., Poza, M., Siles, V.: Towards a certified computation of homology groups for digital images. In: Proceedings 4th International Workshoph on Computational Topology in Image Context (CTIC 2012). LNCS (to appear, 2012)"},{"key":"15_CR16","unstructured":"Heras, J., Mata, G., Poza, M., Rubio, J.: Homological processing of biomedical digital images: automation and certification. In: 17th International Conferences on Applications of Computer Algebra. Computer Algebra in Algebraic Topology and its Applications Session (2011)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-20551-4_3","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J. Heras","year":"2011","unstructured":"Heras, J., Pascual, V., Rubio, J.: Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol.\u00a06564, pp. 37\u201351. Springer, Heidelberg (2011)"},{"key":"15_CR18","unstructured":"Jacobson, N.: Basic Algebra II, 2nd edn. W. H. Freeman and Company (1989)"},{"issue":"1","key":"15_CR19","first-page":"255","volume":"13","author":"S.P. Jones","year":"2003","unstructured":"Jones, S.P., et al.: The Haskell 98 language and libraries: The revised report. Journal of Functional Programming\u00a013(1), 0\u2013255 (2003), \n                    \n                      http:\/\/www.haskell.org","journal-title":"Journal of Functional Programming"},{"key":"15_CR20","unstructured":"Kaufmann, M., Moore, J.S.: ACL2 version 4.3 (2011)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-22863-6_16","volume-title":"Interactive Theorem Proving","author":"L. Lamb\u00e1n","year":"2011","unstructured":"Lamb\u00e1n, L., Mart\u00edn-Mateos, F.J., Rubio, J., Ruiz-Reina, J.L.: Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 200\u2013215. Springer, Heidelberg (2011)"},{"key":"15_CR22","unstructured":"M\u00f6rtberg, A.: Constructive algebra in functional programming and type theory. In: Mathematics, Algorithms and Proofs 2010 (2010), \n                    \n                      http:\/\/wiki.portal.chalmers.se\/cse\/pmwiki.php\/ForMath\/PapersAndSlides"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Romero, A., Rubio, J.: Homotopy groups of suspended classifying spaces: an experimental approach. To be published in Mathematics of Computation (2012)","DOI":"10.1090\/S0025-5718-2013-02680-4"},{"key":"15_CR24","unstructured":"Romero, A., Sergeraert, F.: Discrete Vector Fields and Fundamental Algebraic Topology (2010), \n                    \n                      http:\/\/arxiv.org\/abs\/1005.5685v1"},{"issue":"5","key":"15_CR25","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. Bulletin des Sciences Math\u00e9matiques\u00a0126(5), 389\u2013412 (2002)","journal-title":"Bulletin des Sciences Math\u00e9matiques"}],"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-31374-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T09:22:03Z","timestamp":1556875323000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}