{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T05:10:06Z","timestamp":1685077806039},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2009,7,29]],"date-time":"2009-07-29T00:00:00Z","timestamp":1248825600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2009,8]]},"DOI":"10.1007\/s10472-009-9156-3","type":"journal-article","created":{"date-parts":[[2009,7,28]],"date-time":"2009-07-28T06:14:45Z","timestamp":1248761685000},"page":"273-296","source":"Crossref","is-referenced-by-count":4,"title":["Invariants for the FoCaL language"],"prefix":"10.1007","volume":"56","author":[{"given":"Renaud","family":"Rioboo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,7,29]]},"reference":[{"issue":"2","key":"9156_CR1","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G Barthe","year":"2003","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261\u2013293 (2003)","journal-title":"J. Funct. Program."},{"key":"9156_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. Springer, New York (2004)"},{"key":"9156_CR3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007","author":"R Bonichon","year":"2007","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007. Springer, New York (2007)"},{"key":"9156_CR4","unstructured":"Boulm\u00e9, S.: Sp\u00e9cification d\u2019un environnement d\u00e9di\u00e9 \u00e0 la programmaion certifi\u00e9e de biblioth\u00e8ques de Calcul Formel. Th\u00e8se de doctorat, Universit\u00e9 Paris 6 (2000)"},{"key":"9156_CR5","unstructured":"Boulm\u00e9, S., Hardin, T., Rioboo, R.: Some hints for polynomials in the Foc project. In: Calculemus 2001 Proceedings, June 2001"},{"key":"9156_CR6","first-page":"554","volume-title":"Proceedings of the 10th Annual Conference of the EACSL","author":"P Courtieu","year":"2001","unstructured":"Courtieu, P.: Normalized types. In: Fribourg, L. (ed.) Proceedings of the 10th Annual Conference of the EACSL, pp. 554\u2013569. Springer, New York (2001)"},{"key":"9156_CR7","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-corn, the constructive coq repository at Nijmegen. In: Mathematical Knowledge Management. LNCS, vol. 3119, pp. 88\u2013103, September 2004","DOI":"10.1007\/978-3-540-27818-4_7"},{"key":"9156_CR8","doi-asserted-by":"crossref","unstructured":"Dubois, C., Hardin, T., Donzeau-Gouge, V.: Building certified components within FoCaL. In: Revised Selected Papers from the Fifth Symposium on Trends in Functional Programming, TFP 2004, pp. 33\u201348 (2006)","DOI":"10.2307\/j.ctv36xw0k5.6"},{"key":"9156_CR9","unstructured":"Fechter, S.: S\u00e9mantique des traits orient\u00e9s objet de Focal. Th\u00e8se de doctorat, Universit\u00e9 Paris 6, Juillet (2005)"},{"key":"9156_CR10","volume-title":"Algorithms for Computer Algebra","author":"KO Geddes","year":"1993","unstructured":"Geddes, K.O., Czapor, S.R., Labahn, G.: Algorithms for Computer Algebra. Kluwer Academic, Dordrecht (1993)"},{"issue":"4","key":"9156_CR11","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1006\/jsco.2002.0552","volume":"34","author":"H Geuvers","year":"2002","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput. 34(4), 271\u2013286 (2002)","journal-title":"J. Symb. Comput."},{"key":"9156_CR12","doi-asserted-by":"crossref","unstructured":"Hardin, T., Rioboo, R.: Les objets des math\u00e9matiques. RSTI\u2014L\u2019objet, Octobre 2004","DOI":"10.3166\/objet.10.4.83-118"},{"key":"9156_CR13","volume-title":"Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003)","author":"D Hickey","year":"2002","unstructured":"Hickey, D., Nogin, A., Constable, L., Aydemir, B., Barzilay, B., Bryukhov, Y., Eaton, R., Granicz, A., Kopylov, A., Kreitz, C., Krupski, V., Lorigo, L., Schmitt, S., Witty, S., Yu, X.: Metaprl a modular logical environment. In: Carre\u00f1o, V., Mu\u00f1oz, C., Tahar, S. (eds.) Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Springer, New York (2002)"},{"key":"9156_CR14","unstructured":"Homeier, P.V.: Quotient types. In: Jackson, P., Boulton, R. (eds.) TPHOLs 2001: Supplemental Proceedings, September 2001"},{"key":"9156_CR15","volume-title":"AXIOM: The Scientific Computation System","author":"RD Jenks","year":"1992","unstructured":"Jenks, R.D., Sutor, R.: AXIOM: The Scientific Computation System. Springer, New York (1992)"},{"issue":"7","key":"9156_CR16","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1080\/00029890.1995.12004627","volume":"102","author":"L Lamport","year":"1995","unstructured":"Lamport, L.: How to write a proof. Am. Math. Mon. 102(7), 600\u2013608 (1995)","journal-title":"Am. Math. Mon."},{"key":"9156_CR17","volume-title":"Algebra","author":"S Lang","year":"1969","unstructured":"Lang, S.: Algebra. Addison-Wesley, Reading (1969)"},{"key":"9156_CR18","volume-title":"Algebra","author":"S MacLane","year":"1967","unstructured":"MacLane, S., Birkhoff, G.: Algebra. Macmillan, New York (1967)"},{"key":"9156_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, London (2002)"},{"key":"9156_CR20","volume-title":"Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002)","author":"A Nogin","year":"2002","unstructured":"Nogin, A.: Quotient types: a modular approach. In: Basin, D., Wolff, B. (eds.) Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002). Springer, New York (2002)"},{"key":"9156_CR21","unstructured":"Owre, S., Shankar, N.: Theory interpretations in pvs. CSL Technical Report SRI-CSL-01-01, http:\/\/pvs.csl.sri.com\/doc\/interpretations.pdf (2001)"},{"issue":"4","key":"9156_CR22","doi-asserted-by":"crossref","first-page":"658","DOI":"10.1145\/1183278.1183280","volume":"7","author":"LC Paulson","year":"2006","unstructured":"Paulson, L.C.: Defining functions on equivalence classes. ACM Trans. Comput. Log. 7(4), 658\u2013675 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"9156_CR23","unstructured":"Prevosto, V.: Conception et implantation du langage FoC pour le d\u00e9veloppement de logiciels certifi\u00e9s. Th\u00e8se de doctorat, Universit\u00e9 Paris 6, September 2003"},{"issue":"3\u20134","key":"9156_CR24","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1023\/A:1021979218446","volume":"29","author":"V Prevosto","year":"2002","unstructured":"Prevosto, V., Doligez, D.: Algorithms and proof inheritance in the FoC language. J. Autom. Reason. 29(3\u20134), 337\u2013363 (2002)","journal-title":"J. Autom. Reason."},{"key":"9156_CR25","series-title":"LNCS","first-page":"324","volume-title":"TLCA","author":"V Prevosto","year":"2005","unstructured":"Prevosto, V., Sylvain, B.: Proof contexts with late binding. In: Urzyczyn, P. (ed.) TLCA. LNCS, vol. 3461, pp. 324\u2013338, Nara, Japan. Springer, New York (2005)"},{"key":"9156_CR26","unstructured":"The OpenAxiom Project. http:\/\/www.open-axiom.org\/ (2005)"},{"key":"9156_CR27","unstructured":"The FoCaL Projet. http:\/\/focal.inria.fr\/ (2003)"},{"key":"9156_CR28","unstructured":"The ARC quotient. http:\/\/quotient.inria.fr (2005)"},{"key":"9156_CR29","unstructured":"The ACI Ssurf. http:\/\/www-spi.lip6.fr\/~jaume\/ssurf.html (2006)"},{"key":"9156_CR30","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual Version 8. INRIA-Rocquencourt, Le Chesnay (2006)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9156-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-009-9156-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9156-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T04:43:42Z","timestamp":1685076222000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-009-9156-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,7,29]]},"references-count":30,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["9156"],"URL":"https:\/\/doi.org\/10.1007\/s10472-009-9156-3","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,7,29]]}}}