{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:07:41Z","timestamp":1725484061532},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540432876"},{"type":"electronic","value":"9783540458425"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45842-5_14","type":"book-chapter","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T20:00:38Z","timestamp":1180209638000},"page":"217-232","source":"Crossref","is-referenced-by-count":4,"title":["Generalization in Type Theory Based Proof Assistants"],"prefix":"10.1007","author":[{"given":"Olivier","family":"Pons","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"key":"14_CR1","unstructured":"D. Aspinall, et al. Proof general 3.0, December 1999. http:\/\/www.proofgeneral.org ."},{"key":"14_CR2","unstructured":"B. Barras, et al. The Coq Proof Assistant Reference Manual. INRIA, December 1999. Version 6.3.1."},{"key":"14_CR3","unstructured":"J. Bertot, et al. User guide to the CtCoq proof environment. Rapport technique RT0210, INRIA, 1997."},{"key":"14_CR4","unstructured":"O. Boite. Proving type soundness of simply typed ml-like language with references. In Supplementary Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u20192001), September 2001."},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/3-540-45315-6_4","volume-title":"Type Isomorphisms and Proof Reuse in Dependent Type Theory","author":"G. Barthe","year":"2001","unstructured":"G. Barthe and O. Pons. Type Isomorphisms and Proof Reuse in Dependent Type Theory. In F. Honsell and M. Miculan, editors, Proceedings of FOSSACS 2001, LNCS 2030, pages 57\u201371. Springer, 2001."},{"key":"14_CR6","unstructured":"R. Constable, et al. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, 1986."},{"key":"14_CR7","unstructured":"R\u00e9gis Curien. Outils pour la preuve par analogie. Th\u00e8se de doctorat, Universite\u00e9 Henri Poincar\u00e9, Nancy I, 1995."},{"key":"14_CR8","unstructured":"J. Denzinger, M. Fuchs, C. Goller, and S. Schul. Learning from previous proof experience: a survey. Technical report, Technischen Universit\u00e4t M\u00fcnchen, 1999."},{"key":"14_CR9","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Generalization and reuse of tactic proofs","author":"A. Felty","year":"1994","unstructured":"A. Felty and D. Howe. Generalization and reuse of tactic proofs. LNCS 822, 1\u201315, 1994."},{"key":"14_CR10","unstructured":"R. Hasker and U. Reddy. Generalization at higher types. In D. Miller, editor, Proceedings of the Workshop on the \u03bbProlog Programming Language, pages 257\u2013271, Philadelphia, Pennsylvania, July 1992. University of Pennsylvania. Available as Technical Report MS-CIS-92-86."},{"key":"14_CR11","unstructured":"T. Kolbe and C. Walther. Reusing proofs. In Proc. of the 11th ECAI, pages 80\u201384, Amsterdam, The Netherlands, 1994."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"T. Kolbe and C. Walther. Patching proofs for reuse. In N. Lavrac and S. Wrobel, editors, Proceeding of the European Conference on Machine Learning (ECML-95), Springer LNAI 912, pages 303\u2013306. Heraklion, Greece, 1995.","DOI":"10.1007\/3-540-59286-5_73"},{"key":"14_CR13","unstructured":"N. Magaud and Y. Bertot. Changement de repr\u00e9sentation des structures de donn\u00e9es en Coq: le cas des entiers naturels. In JFLA 2001, 2001."},{"key":"14_CR14","unstructured":"E. Melis. a model of analogy-driven proof-plan construction. In Frank Pfenning, editor, Proceedings of the 14th International Joint Conference on Artificial Intelligence, pages 182\u2013189, Montreal, 1995."},{"key":"14_CR15","unstructured":"E. Melis. AI-techniques in proof planning. In European Conference on Artificial Intelligence, pages 494\u2013498, 1998."},{"key":"14_CR16","unstructured":"O. Pons, Y. Bertot, and L. Rideau. Notions of dependency in proof assistants. In Electronic Proceedings of \u201cUser Interfaces for Theorem Provers 1998 \u201d, Sophia-Antipolis, France, 1998."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74\u201385, Amsterdam, The Netherlands, July 1991.","DOI":"10.1109\/LICS.1991.151632"},{"key":"14_CR18","unstructured":"G. D. Plotkin. A note on inductive generalization. In B. Meltzer and D. Michie, editors, Machine Intelligence 5, pages 153\u2013163, Edinburgh, 1969. Edinburgh University Press."},{"key":"14_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/3-540-57529-4_61","volume-title":"Foundation of Software Technology and Theoretical Computer Science","author":"W. Reif","year":"1993","unstructured":"W. Reif and K. Stenzel. Reuse of Proofs in Software Verification. In R. Shyamasundar, editor, Foundation of Software Technology and Theoretical Computer Science. Proceedings, Springer LNCS 761, pages 284\u2013293. Bombay, India, 1993."},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"M. Si. and T. Reps. Program generalization for software reuse: From C to C++. In Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, volume 216 of ACM Software Engineering Notes, pages 135\u2013146, New York, October 16\u201318 1996. ACM Press.","DOI":"10.1145\/250707.239121"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"L. Th\u00e9ry. A certified version of Buchberger\u2019s algorithm. In Automated Deduction (CADE-15), LNAI 1421, Springer-Verlag, July 1998.","DOI":"10.1007\/BFb0054271"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45842-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T07:03:08Z","timestamp":1556434988000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}