{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:23Z","timestamp":1749125183822},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_62","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:40:08Z","timestamp":1330292408000},"page":"317-331","source":"Crossref","is-referenced-by-count":11,"title":["Efficient second-order matching"],"prefix":"10.1007","author":[{"given":"R\u00e9gis","family":"Curien","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenyu","family":"Qian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hui","family":"Shi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"25_CR1","unstructured":"T. Boy de la Tour and R. Caferra. Proof analogy in interactive theorem proving: A method to express and use it via second order pattern matching. In proceedings of AAAI'87, 1987."},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour and R. Caferra. A formale approach to some usually informal techniques used in mathematical reasoning. In ISSAC'88, pages 402\u2013406. Lecture Notes in Computer Science, 1988.","DOI":"10.1007\/3-540-51084-2_38"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"R. S. Boyer and J. S. Moore. A Theorem Prover for a Computational Logic. In Proc. of the 10th International Conference on Automated Deduction, 1990.","DOI":"10.1007\/3-540-52885-7_75"},{"key":"25_CR4","volume-title":"PhD thesis","author":"R. Curien","year":"1995","unstructured":"R. Curien. Outils pour la preuve par analogie. PhD thesis, Universit\u00e9 Henri Poincar\u00e9 \u2014 Nancy 1, January 1995."},{"key":"25_CR5","unstructured":"R. Curien. Second Order E-matching as a Tool for Automated Theorem Proving. In Proceedings of EPIA '93 (Portugese Conference on Artificial Intelligence) Porto, Portugal., volume 727 of Lecture Notes in Artificial Intelligence, 93."},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"R. Curien and Z. Qian. Efficiency for second-order matching: the syntactic and AC-cases. Technical report, 1995. Draft paper.","DOI":"10.1007\/3-540-61464-8_62"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"G. Dowek. A Second-order Pattern Matching Algorithm in the Cube of Typed \u03bb-calculi. In Mathematical Fundation of Computer Science, LNCS 520, 1991.","DOI":"10.1007\/3-540-54345-7_58"},{"key":"25_CR8","unstructured":"R. Harper, D. MacQueen, and R. Milner. Standard ML. Technical report, Dept. of Cmputer Science, University of Edinburg, 1986."},{"key":"25_CR9","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"25_CR10","volume-title":"Th\u00e8se de Doctorat d'Etat","author":"G. Huet","year":"1976","unstructured":"G. Huet. R\u00e9solution d'Equations dans les langages d'Ordre 1,2, ...,\u03c9. Th\u00e8se de Doctorat d'Etat, Universit\u00e9 de Paris 7 (France), 1976."},{"key":"25_CR11","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31\u201355, 1978.","journal-title":"Acta Informatica"},{"key":"25_CR12","unstructured":"T. Kolbe and C. Walther. Reusing proofs. In A. Cohn, editor, ECAI'94, 11th European Conference on Artificial Intelligence, pages 80\u201384, 1994."},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"B. Krieg-Br\u00fcchner, J. Liu, H. Shi, and B. Wolff. Towards correct, effficient and reusable transformational developments. In \u201dKORSO: Methods, Languages, and Tools for the Construction of Correct Software\u201d, ages 270\u2013284. LNCS 1009, 1995.","DOI":"10.1007\/BFb0015467"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"T. Nipkow and Z. Qian. Modular higher-order E-unification. In R. Book, editor, Proc. 4th Int. Conf. Rewriting Techniques and Applications, pages 200\u2013214. LNCS 488, 1991.","DOI":"10.1007\/3-540-53904-2_97"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"L. Paulson. Isabelle \u2014 A Generic Theorem prover. LNCS 828, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"25_CR16","unstructured":"Z. Qian and K. Wang. Higher-order E-unification for arbitrary theories. In K. Apt, ed., Proc. 1992 Joint Int. Conf. and Symp. on Logic Programming. MIT Press, 1992."},{"key":"25_CR17","unstructured":"H. Shi. Extended Matching with Applications to Program Transformation. PhD thesis, Universit\u00e4t Bremen, 1994."},{"key":"25_CR18","first-page":"573","volume":"449","author":"W. Snyder","year":"1990","unstructured":"W. Snyder. Higher-order E-unification. In M. Stickel, editor, Proc. 10th Int. Conf. Automated Deduction, pages 573\u2013587. Springer-Verlag LNCS 449, 1990.","journal-title":"Springer-Verlag LNCS"},{"issue":"1","key":"25_CR19","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"W. Snyder and J. Gallier. Higher-order unification revisited: Complete sets of transformations. J. Symbolic Computation, 8(1 & 2):101\u2013140, 1989.","journal-title":"J. Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_62.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:06:31Z","timestamp":1605647191000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_62"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_62","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}