{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:57:22Z","timestamp":1725533842536},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026133"},{"type":"electronic","value":"9783642026140"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02614-0_13","type":"book-chapter","created":{"date-parts":[[2009,7,2]],"date-time":"2009-07-02T11:47:24Z","timestamp":1246535244000},"page":"106-121","source":"Crossref","is-referenced-by-count":7,"title":["ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System"],"prefix":"10.1007","author":[{"given":"Francisco-Jesus","family":"Mart\u00edn-Mateos","sequence":"first","affiliation":[]},{"given":"Julio","family":"Rubio","sequence":"additional","affiliation":[]},{"given":"Jose-Luis","family":"Ruiz-Reina","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","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, vol.\u00a04573, pp. 1\u201312. Springer, Heidelberg (2007)"},{"key":"13_CR2","unstructured":"Andr\u00e9s, M., Lamb\u00e1n, L., Rubio, J., Ruiz-Reina, J.L.: Formalizing Simplicial Topology in ACL2. In: ACL2 Workshop 2007, University of Austin, pp. 34\u201339 (2007)"},{"key":"13_CR3","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, 271\u2013292 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/11556985_21","volume-title":"Computer Aided Systems Theory \u2013 EUROCAST 2005","author":"J. Aransay","year":"2005","unstructured":"Aransay, J., Ballarin, C., Rubio, J.: Extracting Computer Algebra Programs from Statements. In: Moreno D\u00edaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2005. LNCS, vol.\u00a03643, pp. 159\u2013168. Springer, Heidelberg (2005)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","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, vol.\u00a04573, pp. 40\u201354. Springer, Heidelberg (2007)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-540-85110-3_23","volume-title":"Intelligent Computer Mathematics","author":"C. Dom\u00ednguez","year":"2008","unstructured":"Dom\u00ednguez, C.: Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS, vol.\u00a05144, pp. 270\u2013284. Springer, Heidelberg (2008)"},{"key":"13_CR7","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 - Theoretical Informatics and Applications\u00a041, 191\u2013214 (2007)","journal-title":"Rairo - Theoretical Informatics and Applications"},{"key":"13_CR8","unstructured":"Dousson, X., Rubio, J., Sergeraert, F., Siret, Y.: The Kenzo Program, Institut Fourier (1999), \n                    \n                      http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo\/"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-540-85110-3_37","volume-title":"Intelligent Computer Mathematics","author":"J. Heras","year":"2008","unstructured":"Heras, J., Pascual, V., Rubio, J.: Mediated Access to Symbolic Computation Systems. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS, vol.\u00a05144, pp. 446\u2013461. Springer, Heidelberg (2008)"},{"key":"13_CR10","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"13_CR11","unstructured":"Kaufmann, M., Moore, J S.: ACL2 Home Page, \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/moore\/acl2"},{"key":"13_CR12","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. Applicable Algebra in Engineering, Communication and Computing\u00a014, 187\u2013215 (2003)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"13_CR13","unstructured":"Mart\u00edn\u2013Mateos, F.J., Ruiz\u2013Reina, J.L., Rubio, J.: ACL2 verification of simplicial degeneracy programs in the Kenzo system, \n                    \n                      http:\/\/www.cs.us.es\/~fmartin\/acl2\/kenzo"},{"key":"13_CR14","unstructured":"May, J.P.: Simplicial Objects in Algebraic Topology. Van Nostrand (1967)"},{"key":"13_CR15","unstructured":"Rubio, J., Sergeraert, F., Siret, Y.: EAT: Symbolic Software for Effective Homology Computation, Institut Fourier (1997), \n                    \n                      ftp:\/\/ftp-fourier.ujf-grenoble.fr\/pub\/EAT"},{"key":"13_CR16","unstructured":"Steele Jr., G.L.: Common Lisp The Language, 2nd edn. Digital Press (1990)"}],"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-02614-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T01:47:51Z","timestamp":1552096071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02614-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026133","9783642026140"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02614-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}