{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T04:03:55Z","timestamp":1725595435206},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642226724"},{"type":"electronic","value":"9783642226731"}],"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_2","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T11:49:15Z","timestamp":1310557755000},"page":"15-29","source":"Crossref","is-referenced-by-count":0,"title":["Retargeting OpenAxiom to Poly\/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework"],"prefix":"10.1007","author":[{"given":"Gabriel","family":"Dos Reis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Matthews","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yue","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/231191.231194","volume":"30","author":"J. Abbott","year":"1996","unstructured":"Abbott, J., D\u00edaz, A., Sutor, R.S.: A report on openmath: a protocol for the exchange of mathematical information. SIGSAM Bull.\u00a030, 21\u201324 (1996)","journal-title":"SIGSAM Bull."},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/3-540-44755-5_4","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Adams","year":"2001","unstructured":"Adams, A., Dunstan, M., Gottliebsen, H., Kelsey, T., Martin, U., Owre, S.: Computer algebra meets automated theorem proving: Integrating maple and pvs. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 27\u201342. Springer, Heidelberg (2001)"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1145\/220346.220366","volume-title":"Proceedings of the 1995 international symposium on Symbolic and algebraic computation, ISSAC 1995","author":"C. Ballarin","year":"1995","unstructured":"Ballarin, C., Homann, K., Calmet, J.: Theorems and algorithms: an interface between isabelle and maple. In: Proceedings of the 1995 international symposium on Symbolic and algebraic computation, ISSAC 1995, pp. 150\u2013157. ACM, New York (1995)"},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1006\/jsco.2001.0455","volume":"32","author":"H. Barendregt","year":"2001","unstructured":"Barendregt, H., Cohen, A.M.: Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants. J. Symb. Comput.\u00a032, 3\u201322 (2001)","journal-title":"J. Symb. Comput."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Calmet, J., Homann, K.: Classification of communication and cooperation mechanisms for logical and symbolic computation systems. In: Frontiers of Combining Systems (FroCos), pp. 221\u2013234 (1996)","DOI":"10.1007\/978-94-009-0349-4_11"},{"key":"2_CR6","unstructured":"Carette, J., Farmer, W.M., Wajs, J.: Trustable communication between mathematics systems. In: Proc. of Calculemus 2003, Aracne, pp. 58\u201368 (2003)"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1017\/S0956796801004282","volume":"12","author":"K. Crary","year":"2002","unstructured":"Crary, K., Weirich, S., Morrisett, G.: Intensional Polymorphism in Type-erasure Semantics. J. Funct. Program.\u00a012, 567\u2013600 (2002)","journal-title":"J. Funct. Program."},{"key":"2_CR8","unstructured":"Davenport, J.H.: A New Algebra System. Technical report, IBM Research (1984)"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1006\/jsco.2002.0551","volume":"34","author":"J.H. Davenport","year":"2002","unstructured":"Davenport, J.H.: Equality in Computer Algebra and Beyond. J. Symb. Comput.\u00a034, 259\u2013270 (2002)","journal-title":"J. Symb. Comput."},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1016\/j.jsc.2004.12.004","volume":"39","author":"D. Delahaye","year":"2005","unstructured":"Delahaye, D., Mayero, M.: Dealing with algebraic expressions over a field in coq using maple. J. Symb. Comput.\u00a039, 569\u2013592 (2005)","journal-title":"J. Symb. Comput."},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A skeptic\u2019s approach to combining hol and maple. J. Autom. Reason.\u00a021, 279\u2013294 (1998)","journal-title":"J. Autom. Reason."},{"key":"2_CR12","unstructured":"Isabelle (2011), \n                    \n                      http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html"},{"key":"2_CR13","volume-title":"AXIOM: The Scientific Computation System","author":"R.D. Jenks","year":"1992","unstructured":"Jenks, R.D., Sutor, R.S.: AXIOM: The Scientific Computation System. Springer, Heidelberg (1992)"},{"key":"2_CR14","first-page":"98","volume-title":"PASCO 2010: Proceedings of the 4th International Workshop on Parallel and Symbolic Computation","author":"Y. Li","year":"2010","unstructured":"Li, Y., Reis, G.D.: A Quantitative Study of Reductions in Algebraic Libraries. In: PASCO 2010: Proceedings of the 4th International Workshop on Parallel and Symbolic Computation, pp. 98\u2013104. ACM, New York (2010)"},{"key":"2_CR15","volume-title":"ISSAC 2011: Proceedings of the International Symposium on Symbolic and Algebraic Computation","author":"Y. Li","year":"2011","unstructured":"Li, Y., Reis, G.D.: An Automatic Parallelization Framework for Algebraic Computation Systems. In: ISSAC 2011: Proceedings of the International Symposium on Symbolic and Algebraic Computation. ACM, New York (2011)"},{"key":"2_CR16","unstructured":"Maple. Maplesoft Inc., Canada (2011), \n                    \n                      http:\/\/www.maplesoft.com"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1145\/1708046.1708058","volume-title":"Proceedings of the 5th ACM SIGPLAN workshop on Declarative aspects of multicore programming, DAMP 2010","author":"D.C.J. Matthews","year":"2010","unstructured":"Matthews, D.C.J., Wenzel, M.: Efficient Parallel Programming in Poly\/ML and Isabelle\/ML. In: Proceedings of the 5th ACM SIGPLAN workshop on Declarative aspects of multicore programming, DAMP 2010, pp. 53\u201362. ACM, New York (2010)"},{"key":"2_CR18","unstructured":"Monagan, M.B., Geddes, K.O., Heal, K.M., Labahn, G., Vorkoetter, S.M., McCarron, J., De Marco, P.: Maple Advanced Programming Guide, Maplesoft, Canada (2007)"},{"key":"2_CR19","unstructured":"OpenAxiom (2011), \n                    \n                      http:\/\/www.open-axiom.org"},{"key":"2_CR20","unstructured":"Poly\/ML (2011), \n                    \n                      http:\/\/www.polyml.org"},{"key":"2_CR21","unstructured":"Watt, S.M.: Aldor Programming Language (December 2009), \n                    \n                      http:\/\/www.aldor.org"},{"key":"2_CR22","unstructured":"Watt, S.M., Broadbery, P.A., Iglio, P., Morrison, S.C., Steinbach, J.M.: Foam: A first order abstract machine version 0.35. Technical report, IBM Thomas J. Watson Research Center (2001)"}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T01:42:40Z","timestamp":1553910160000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}