{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T04:03:58Z","timestamp":1725595438330},"publisher-location":"Berlin, Heidelberg","reference-count":24,"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_6","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T07:49:15Z","timestamp":1310543355000},"page":"74-89","source":"Crossref","is-referenced-by-count":2,"title":["View of Computer Algebra Data from Coq"],"prefix":"10.1007","author":[{"given":"Vladimir","family":"Komendantsky","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Konovalov","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Linton","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1023\/A:1022907629104","volume":"38","author":"A. Asperti","year":"2003","unstructured":"Asperti, A., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical knowledge management in HELM. Annals of Mathematics and Artificial Intelligence\u00a038, 27\u201346 (2003)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-03153-3_4","volume-title":"Language Engineering and Rigorous Software Development","author":"Y. Bertot","year":"2009","unstructured":"Bertot, Y.: Structural abstract interpretation: A formal study using Coq. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) Language Engineering and Rigorous Software Development. LNCS, vol.\u00a05520, pp. 153\u2013194. Springer, Heidelberg (2009)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Guilhot, F., Mahboubi, A.: A formal study of Bernstein coefficients and polynomials. Mathematical Structures in Computer Science (2011)","DOI":"10.1017\/S0960129511000090"},{"issue":"3","key":"6_CR4","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1016\/S1571-0661(05)80609-7","volume":"23","author":"S. Boulm\u00e9","year":"1999","unstructured":"Boulm\u00e9, S., Hardin, T., Hirschkoff, D., M\u00e9nissier-Morain, V., Rioboo, R.: On the way to certify computer algebra systems. Electronic Notes in Theoretical Computer Science\u00a023(3), 370\u2013385 (1999); CALCULEMUS 1999, Systems for Integrated Computation and Deduction (associated to FLoC 1999, the 1999 Federated Logic Conference)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/281508.281540","volume-title":"ISSAC 1998: Proceedings of the 1998 international symposium on Symbolic and algebraic computation","author":"T. Breuer","year":"1998","unstructured":"Breuer, T., Linton, S.: The GAP 4 type system: organising algebraic algorithms. In: ISSAC 1998: Proceedings of the 1998 international symposium on Symbolic and algebraic computation, pp. 38\u201345. ACM, New York (1998)"},{"key":"6_CR6","unstructured":"Caprotti, O., Geuvers, H., Oostdijk, M.: Certified and portable mathematical documents from formal contexts. In: Electronic Proceedings of the 1st International Workshop on Mathematical Knowledge Management, MKM 2001. RISC, Schloss Hagenberg, Austria (2001)"},{"issue":"1\/2","key":"6_CR7","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1006\/jsco.2001.0457","volume":"32","author":"O. Caprotti","year":"2001","unstructured":"Caprotti, O., Oostdijk, M.: Formal and efficient primality proofs by use of computer algebra oracles. J. Symbolic Computation\u00a032(1\/2), 55\u201370 (2001)","journal-title":"J. Symbolic Computation"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Delahaye, D., Mayero, M.: Quantifier elimination over algebraically closed fields in a proof assistant using a computer algebra system. In: Proc. Calculemus 2005. ENTCS, vol.\u00a0151, pp. 57\u201373 (2006)","DOI":"10.1016\/j.entcs.2005.11.023"},{"key":"6_CR9","unstructured":"Freundt, S., Horn, P., Konovalov, A., Lesseni, S., Linton, S., Roozemond, D.: OpenMath in SCIEnce: Evolving of symbolic computation interaction. In: Davenport, J.H. (ed.) 22nd OpenMath Workshop (July 2009)"},{"key":"6_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-540-85110-3_24","volume-title":"Intelligent Computer Mathematics","author":"S. Freundt","year":"2008","unstructured":"Freundt, S., Horn, P., Konovalov, A., Linton, S., Roozemond, D.: Symbolic computation software composability. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol.\u00a05144, pp. 285\u2013295. Springer, Heidelberg (2008)"},{"key":"6_CR11","unstructured":"The GAP\u00a0Group. GAP \u2013 Groups, Algorithms, and Programming, Version 4.4.12 (2008), http:\/\/www.gap-system.org"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009)"},{"key":"6_CR13","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, INRIA (2011)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11737414_8","volume-title":"Functional and Logic Programming","author":"B. Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L., Werner, B.: A computational approach to pocklington certificates in type theory. In: Hagiya, M. (ed.) FLOPS 2006. LNCS, vol.\u00a03945, pp. 97\u2013113. Springer, Heidelberg (2006)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-642-02614-0_38","volume-title":"Intelligent Computer Mathematics","author":"P. Horn","year":"2009","unstructured":"Horn, P., Roozemond, D.: OpenMath in SCIEnce: SCSCP and POPCORN. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol.\u00a05625, pp. 474\u2013479. Springer, Heidelberg (2009)"},{"key":"6_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-73086-6_8","volume-title":"Towards Mechanized Mathematical Assistants","author":"C. Kaliszyk","year":"2007","unstructured":"Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 94\u2013105. Springer, Heidelberg (2007)"},{"key":"6_CR17","series-title":"ENTCS","volume-title":"Proc. User Interfaces for Theorem Provers (UITP) 2010","author":"V. Komendantsky","year":"2010","unstructured":"Komendantsky, V., Konovalov, A., Linton, S.: Interfacing Coq + Ssreflect with GAP. In: Proc. User Interfaces for Theorem Provers (UITP) 2010. ENTCS, Elsevier, Amsterdam (to appear 2010)"},{"key":"6_CR18","unstructured":"Konovalov, A., Linton, S.: SCSCP \u2013 Symbolic Computation Software Composability Protocol, Version 1.2, GAP package (2010), http:\/\/www.cs.st-andrews.ac.uk\/~alexk\/scscp.htm"},{"key":"6_CR19","unstructured":"Leroy, X.: Proving a compiler: Mechanized verification of program transformations and static analyses. Oregon Programming Languages Summer School (2010), http:\/\/cristal.inria.fr\/~xleroy\/courses\/Eugene-2010\/"},{"key":"6_CR20","unstructured":"OpenMath, http:\/\/www.openmath.org\/"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Sa\u00efbi, A.: Typing algorithm in type theory with inheritance. In: Proc. POPL 1997, pp. 292\u2013301 (1997)","DOI":"10.1145\/263699.263742"},{"key":"6_CR22","unstructured":"Symbolic Computation Software Composability Protocol, http:\/\/www.symbolic-computation.org\/SCSCP"},{"key":"6_CR23","unstructured":"The Coq development team. The Coq proof assistant reference manual, http:\/\/coq.inria.fr\/refman\/"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Views: A way for pattern matching to cohabit with data abstraction. In: POPL, pp. 307\u2013313 (1987)","DOI":"10.1145\/41625.41653"}],"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_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T19:19:35Z","timestamp":1560367175000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}