View of computer algebra data from Coq. (English) Zbl 1335.68232
Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 74-89 (2011).
Summary: Data representation is an important aspect of software composition. It is often the case that different software components are programmed to represent data in the ways which are the most appropriate for their problem domains. Sometimes, converting data from one representation to another is a non-trivial task. This is the case with computer algebra systems and type-theory based interactive theorem provers such as Coq. We provide some custom instrumentation inside Coq to support a computer algebra system (CAS) communication protocol known as SCSCP. We describe general aspects of viewing OpenMath terms produced by a CAS in the calculus of Coq, as well as viewing pure Coq terms in a simpler type system that is behind OpenMath.
For the entire collection see [Zbl 1218.68014].
For the entire collection see [Zbl 1218.68014].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68W30 | Symbolic computation and algebraic computation |
References:
| [1] | Asperti, A., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical knowledge management in HELM. Annals of Mathematics and Artificial Intelligence 38, 27–46 (2003) · Zbl 1025.68080 · doi:10.1023/A:1022907629104 |
| [2] | 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. 5520, pp. 153–194. Springer, Heidelberg (2009) · Zbl 1250.68089 · doi:10.1007/978-3-642-03153-3_4 |
| [3] | Bertot, Y., Guilhot, F., Mahboubi, A.: A formal study of Bernstein coefficients and polynomials. Mathematical Structures in Computer Science (2011) · Zbl 1236.33016 · doi:10.1017/S0960129511000090 |
| [4] | Boulmé, S., Hardin, T., Hirschkoff, D., Ménissier-Morain, V., Rioboo, R.: On the way to certify computer algebra systems. Electronic Notes in Theoretical Computer Science 23(3), 370–385 (1999); CALCULEMUS 1999, Systems for Integrated Computation and Deduction (associated to FLoC 1999, the 1999 Federated Logic Conference) · Zbl 0958.68197 · doi:10.1016/S1571-0661(05)80609-7 |
| [5] | 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–45. ACM, New York (1998) · Zbl 0918.68050 · doi:10.1145/281508.281540 |
| [6] | 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) · Zbl 0982.68167 |
| [7] | Caprotti, O., Oostdijk, M.: Formal and efficient primality proofs by use of computer algebra oracles. J. Symbolic Computation 32(1/2), 55–70 (2001) · Zbl 1044.03503 · doi:10.1006/jsco.2001.0457 |
| [8] | 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. 151, pp. 57–73 (2006) · Zbl 1273.68417 · doi:10.1016/j.entcs.2005.11.023 |
| [9] | 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) |
| [10] | 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. 5144, pp. 285–295. Springer, Heidelberg (2008) · Zbl 1166.68374 · doi:10.1007/978-3-540-85110-3_24 |
| [11] | The GAP Group. GAP – Groups, Algorithms, and Programming, Version 4.4.12 (2008), http://www.gap-system.org |
| [12] | 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. 5674, pp. 327–342. Springer, Heidelberg (2009) · Zbl 1252.68253 · doi:10.1007/978-3-642-03359-9_23 |
| [13] | Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, INRIA (2011) |
| [14] | Grégoire, B., Théry, L., Werner, B.: A computational approach to pocklington certificates in type theory. In: Hagiya, M. (ed.) FLOPS 2006. LNCS, vol. 3945, pp. 97–113. Springer, Heidelberg (2006) · Zbl 1185.68621 · doi:10.1007/11737414_8 |
| [15] | 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. 5625, pp. 474–479. Springer, Heidelberg (2009) · Zbl 1247.68316 · doi:10.1007/978-3-642-02614-0_38 |
| [16] | 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. 4573, pp. 94–105. Springer, Heidelberg (2007) · Zbl 1202.68382 · doi:10.1007/978-3-540-73086-6_8 |
| [17] | 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) · Zbl 1294.68124 |
| [18] | Konovalov, A., Linton, S.: SCSCP – Symbolic Computation Software Composability Protocol, Version 1.2, GAP package (2010), http://www.cs.st-andrews.ac.uk/ alexk/scscp.htm |
| [19] | 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/ |
| [20] | OpenMath, http://www.openmath.org/ · Zbl 1151.68669 |
| [21] | Saïbi, A.: Typing algorithm in type theory with inheritance. In: Proc. POPL 1997, pp. 292–301 (1997) · doi:10.1145/263699.263742 |
| [22] | Symbolic Computation Software Composability Protocol, http://www.symbolic-computation.org/SCSCP · Zbl 1166.68374 |
| [23] | The Coq development team. The Coq proof assistant reference manual, http://coq.inria.fr/refman/ |
| [24] | Wadler, P.: Views: A way for pattern matching to cohabit with data abstraction. In: POPL, pp. 307–313 (1987) · doi:10.1145/41625.41653 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
