{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:46Z","timestamp":1749182806517,"version":"3.41.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1023\/a:1021979218446","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T23:56:29Z","timestamp":1048290989000},"page":"337-363","source":"Crossref","is-referenced-by-count":7,"title":["Algorithms and Proofs Inheritance in the FOC Language"],"prefix":"10.1007","volume":"29","author":[{"given":"Virgile","family":"Prevosto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damien","family":"Doligez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5109772_CR1","first-page":"150","volume-title":"Proceedings of ISSAC","author":"C. Ballarin","year":"1995","unstructured":"Ballarin, C., Homann, K. and Calmet, J.: Theorems and algorithms: An interface between Isabelle and Maple, in A. Levelt (ed.), Proceedings of ISSAC, Montr\u00e9al, Canada, ACM Press, 1995, pp. 150\u2013157."},{"key":"5109772_CR2","unstructured":"Betarte, G.: Dependent record types and formal abstract reasoning: Theory and practice, Ph.D. thesis, University of G\u00f6teborg, 1998."},{"key":"5109772_CR3","unstructured":"Boulm\u00e9, S., Hardin, T. and Rioboo, R.: Polymorphic data types, objects, modules and functors: Is it too much? Research Report 14, LIP6, 2000. Available at http:\/\/www.lip6.fr\/reports\/ lip6.2000.014.html."},{"key":"5109772_CR4","unstructured":"Boulm\u00e9, S., Hardin, T. and Rioboo, R.: Some hints for polynomials in the FOC project, in Calculemus 2001 Proceedings, June 2001."},{"key":"5109772_CR5","unstructured":"Boulm\u00e9, S.: Sp\u00e9cification d'un environnement d\u00e9di\u00e9 \u00e0 la programmation certifi\u00e9e de biblioth\u00e8ques de Calcul Formel, Ph.D. thesis, Universit\u00e9 Paris 6, 2000."},{"key":"5109772_CR6","doi-asserted-by":"crossref","unstructured":"Buchberger, B. et al.: A survey on the Theorema project, in W. Kuechlin (ed.), Proceedings of ISSAC'97, ACM Press, 1997.","DOI":"10.1145\/258726.258853"},{"key":"5109772_CR7","doi-asserted-by":"crossref","unstructured":"Cerioli, M., Mosses, P. and Reggio, G. (eds): Proceedings of the 15th International Workshop on Algebraic Development Techniques and the General Workshop of the CoFI WG, Genova, Italy, April 2001.","DOI":"10.1007\/3-540-45645-7"},{"key":"5109772_CR8","doi-asserted-by":"crossref","unstructured":"Dalmas, S., Ga\u00ebtano, M. and Watt, S.: An OpenMath 1.0 implementation, in W. Kuechlin (ed.), Proceedings of ISSAC'97, ACM Press, 1997.","DOI":"10.1145\/258726.258794"},{"key":"5109772_CR9","unstructured":"Davenport, J., Siret, Y., Tournier, E. and Lazard, D.: Computer Algebra, Masson, 1993."},{"key":"5109772_CR10","unstructured":"Dunstan, M., Gottliebsen, H., Kelsey, T. and Martin, U.: Computer algebra meets automated theorem proving: A Maple-PVS interface, in Proceedings of the Calculemus Workshop, 2001."},{"key":"5109772_CR11","unstructured":"Farmer, W. M., Guttman, J. D. and Thayer, F. J.: The IMPS user's manual, Technical Report M-93B138. The MITRE Corporation, November 1995. Available at ftp:\/\/ math.harvard.edu\/imps\/doc\/."},{"key":"5109772_CR12","unstructured":"Fechter, S.: Une S\u00e9mantique pour FOC, Rapport de D.E.A., Universit\u00e9 Paris 6, Septembre 2001."},{"key":"5109772_CR13","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F. and Zwanenburg, J.: The algebraic hierarchy of the FTA project, in Proceedings of the Calculemus Workshop, 2001."},{"key":"5109772_CR14","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison, J. and Th\u00e9ry, L.: A skeptic's approach to combining HOL and Maple, J. Automated Reasoning\n21 (1998), 279\u2013294.","journal-title":"J. Automated Reasoning"},{"key":"5109772_CR15","doi-asserted-by":"crossref","unstructured":"Jackson, P.: Exploring abstract algebra in constructive type theory, in Proceedings of 12th International Conference on Automated Deduction, 1994.","DOI":"10.1007\/3-540-58156-1_43"},{"key":"5109772_CR16","unstructured":"Jenks, R. D. and Stutor, R. S.: AXIOM, The Scientific Computation System, Springer-Verlag, 1992."},{"key":"5109772_CR17","unstructured":"Leroy, X., Doligez, D., Garrigue, J., R\u00e9my, D. and Vouillon, J.: The Objective Caml system release 3.00 Documentation and user's manual, INRIA, 2000. http:\/\/pauillac.inria.fr\/ ocaml\/htmlman\/."},{"key":"5109772_CR18","unstructured":"Mandel, L.: Factorisation de polyn\u00f4mes sur les corps finis, Rapport de magist\u00e9re, Universit\u00e9 Paris 6, 2001."},{"key":"5109772_CR19","doi-asserted-by":"crossref","unstructured":"Pollack, R.: Dependently typed records for representing mathematical structures, in TPHOLs'00, Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44659-1_29"},{"key":"5109772_CR20","unstructured":"Pottier, L.: Contrib. algebra. http:\/\/coq.inria.fr\/contribs-eng.html."},{"key":"5109772_CR21","unstructured":"Prevosto, V.: Vers une interface utilisateur pour foc, Rapport de D.E.A., Universit\u00e9 Paris 6, Septembre 2000."},{"key":"5109772_CR22","unstructured":"Prevosto, V. and Doligez, D.: Algorithms and proofs inheritance in the FOC language, Research Report, LIP6, 2002 (to appear). Available at http:\/\/www-spi.lip6.fr\/~prevosto\/ papiers\/rr02.ps.gz."},{"key":"5109772_CR23","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual, Projet LogiCal, INRIA-Rocquencourt \u2013 LRI Paris 11, Nov. 1996."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021979218446.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021979218446\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021979218446.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:26:51Z","timestamp":1749122811000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021979218446"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":23,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5109772"],"URL":"https:\/\/doi.org\/10.1023\/a:1021979218446","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}