{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:31:27Z","timestamp":1725489087543},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730835"},{"type":"electronic","value":"9783540730866"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73086-6_1","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T10:57:56Z","timestamp":1187089076000},"page":"1-12","source":"Crossref","is-referenced-by-count":4,"title":["Executing in Common Lisp, Proving in ACL2"],"prefix":"10.1007","author":[{"given":"Mirian","family":"Andr\u00e9s","sequence":"first","affiliation":[]},{"given":"Laureano","family":"Lamb\u00e1n","sequence":"additional","affiliation":[]},{"given":"Julio","family":"Rubio","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Aransay, J., Ballarin, C., Rubio, J.: Towards a Higher Reasoning Level in Formalized Homological Algebra. In: Proceedings Calculemus 2003, Aracn\u00e9 \u00c9ditrice, pp. 84\u201388 (2003)"},{"key":"1_CR2","series-title":"Lecture Notes in Artificial Intelligence","first-page":"221","volume-title":"Artificial Intelligence and Symbolic Computation","author":"J. Aransay","year":"2004","unstructured":"Aransay, J., Ballarin, C., Rubio, J.: Four Approaches to Automated Reasoning with Differential Algebraic Structures. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNCS (LNAI), vol.\u00a03249, pp. 221\u2013234. Springer, Heidelberg (2004)"},{"key":"1_CR3","unstructured":"Aransay, J., Ballarin, C., Rubio, J.: A Mechanized Proof of the Basic Perturbation Lemma. Preprint"},{"key":"1_CR4","unstructured":"Berciano, A., Sergeraert, F.: Software to compute A\n                           \u2009\u221e\u2009-(co)algebras: Araia & Craic (2006), \n                    \n                      http:\/\/www.ehu.es\/aba\/araia-craic.htm"},{"key":"1_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":"1_CR6","doi-asserted-by":"crossref","unstructured":"Boulm\u00e9, S., Hardin, T., Hirschkoff, D., M\u00e9nissier-Morain, V., Rioboo, R.: On the way to certify Computer Algebra systems. In: Proceedings Calculemus 1999, Electronic Notes in Theoretical Computer Science, vol. 23 (1999)","DOI":"10.1016\/S1571-0661(05)80609-7"},{"issue":"2","key":"1_CR7","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"12","key":"1_CR8","first-page":"1701","volume":"12","author":"C. Dom\u00ednguez","year":"2006","unstructured":"Dom\u00ednguez, C., Rubio, J., Sergeraert, F.: Modeling Inheritance as Coercion in the Kenzo System. Journal of Universal Computer Science\u00a012(12), 1701\u20131730 (2006)","journal-title":"Journal of Universal Computer Science"},{"key":"1_CR9","unstructured":"Dom\u00ednguez, C., Lamb\u00e1n, L., Rubio, J.: Object-Oriented Institutions to Specify Symbolic Computation Systems. To appear in Rairo Theoretical Informatics and Applications"},{"key":"1_CR10","unstructured":"Dousson, X., Sergeraert, F., Siret, Y.: The Kenzo program (1999-2007), \n                    \n                      http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo\/"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"200","DOI":"10.2307\/2372629","volume":"75","author":"S. Eilenberg","year":"1953","unstructured":"Eilenberg, S., Zilber, J.A.: On products of complexes. American Journal of Mathematics\u00a075, 200\u2013204 (1953)","journal-title":"American Journal of Mathematics"},{"key":"1_CR12","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston (2000)"},{"issue":"3","key":"1_CR13","first-page":"187","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(3), 187\u2013215 (2003)","journal-title":"Communication and Computing"},{"key":"1_CR14","volume-title":"Homology","author":"S. Mac Lane","year":"1994","unstructured":"Mac Lane, S.: Homology. Springer, Heidelberg (1994)"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF03177742","volume":"32","author":"F.J. Mart\u00edn","year":"2004","unstructured":"Mart\u00edn, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz-Reina, J.L.: Formal verification of a generic framework to synthesize SAT-provers. Journal of Automated Reasoning\u00a032, 287\u2013313 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR16","unstructured":"May, P.: Simplicial Objects in Algebraic Topology, Van Nostrand (1967)"},{"key":"1_CR17","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.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"1059","DOI":"10.1016\/j.jsc.2006.06.002","volume":"41","author":"A. Romero","year":"2006","unstructured":"Romero, A., Rubio, J., Sergeraert, F.: Computing Spectral Sequences. Journal of Symbolic Computation\u00a041, 1059\u20131079 (2006)","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR19","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 Sciences Math\u00e9matiques\u00a0126, 389\u2013412 (2002)","journal-title":"Bulletin Sciences Math\u00e9matiques"},{"key":"1_CR20","unstructured":"Rubio, J., Sergeraert, F.: Constructive Homological Algebra, Lectures Notes MAP Summer School (2006), \n                    \n                      http:\/\/map.disi.unige.it\/summer_school\/index.php?page=2"},{"key":"1_CR21","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"}],"container-title":["Lecture Notes in Computer Science","Towards Mechanized Mathematical Assistants"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73086-6_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:59:39Z","timestamp":1619517579000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730835","9783540730866"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}