{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:21Z","timestamp":1761611301183,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"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_47","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:39:41Z","timestamp":1330292381000},"page":"123-137","source":"Crossref","is-referenced-by-count":2,"title":["Higher-order superposition for dependent types"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Virga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Coquand, T. An algorithm for Testing Conversion in Type Theory. Logical Frameworks, Cambridge University Press, 1991, pages 155\u2013279","DOI":"10.1017\/CBO9780511569807.011"},{"key":"10_CR2","volume-title":"Ph.D. Thesis","author":"W. Gehrke","year":"1995","unstructured":"Gehrke, W., Decidability Results For Categorical Notions Related to Monads by Rewriting Techniques Ph.D. Thesis, Johannes Kepler Universit\u00e4t, Linz, 1995"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Geuvers, H. The Church-Rosser Property for \u03b2\u03b7-Reduction in Typed \u03bb-Calculi. Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science (LICS), 1992, pages 453\u2013460","DOI":"10.1109\/LICS.1992.185556"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Harper, R., Honsell F., Plotkin, G. A framework for Defining Logics. Journal of the Association for Computing Machinery, January 1993, pages 143\u2013184","DOI":"10.1145\/138027.138060"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G.P. Huet","year":"1978","unstructured":"Huet, G.P., Lang, B. Proving and Applying Program Transformations Expressed with Second-Order Patterns Acta Informatica 11, 1978, pages 31\u201355","journal-title":"Acta Informatica"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Kahrs, D. Towards a Domain Theory for Termination Proofs. Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA), 1995, pages 241\u2013255","DOI":"10.1007\/3-540-59200-8_60"},{"key":"10_CR7","unstructured":"Knuth, D.E., Bendix, P.B. Simple Word Problems in Universal Algebra. Computational Problems in Abstract Algebra, Pergamon Press, 1972, pages 263\u2013297"},{"key":"10_CR8","unstructured":"Lor\u00eda-S\u00e1enz, C. A. A Theoretical Framework for Reasoning about Program Construction Based on Extensions of Rewrite Systems Ph.D. Thesis, Universit\u00e4t Kaiserslautern, 1993"},{"key":"10_CR9","unstructured":"Mayr, R., Nipkow, T. Higher-Order Rewrite Systems and their Confluence. Technical Report TUM-I9433, Technische Universit\u00e4t M\u00fcnchen, 1994"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Miller, D. A Logic Programming Language With Lambda abstraction, Function Variables, and Simple Unification. LFCS Report Series, University of Edinburgh, 1991, pages 253\u2013281","DOI":"10.1007\/BFb0038698"},{"issue":"2","key":"10_CR11","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M.H.A. Newman","year":"1942","unstructured":"Newman, M.H.A. On theories with a combinatorial definition of \u2018equivalence' Annals of Mathematics, 43(2), 1942, pages 223\u2013243","journal-title":"Annals of Mathematics"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Nipkow, T. Higher-Order Critical Pairs. Proceedings of the 5th IEEE Conference of Logic In Computer Science (LICS), 1990, pages 342\u2013348","DOI":"10.1109\/LICS.1991.151658"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L.C. Paulson","year":"1989","unstructured":"Paulson, L.C. The Foundation of a Generic Theorem Prover Journal of Automated Reasoning, vol. 5, 1989, pages 363\u2013397","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Pfenning, F. Logic Programming in the LF Logical Framework. G. Huet, G. Plotkin ed., Logical Frameworks, Cambridge University Press, 1991, pages 149\u2013181","DOI":"10.1017\/CBO9780511569807.008"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Pfenning, F. Unification and anti-unification in the Calculus of Constructions., Proceedings of the 6th IEEE Conference of Logic In Computer Science (LICS), 1991, pages 149\u2013181","DOI":"10.1109\/LICS.1991.151632"},{"key":"10_CR16","unstructured":"Pfenning, F. A Structural Proof of Cut Elimination and Its Representation in a Logic Framework Technical Report CMU-CS-94-218, Carnegie Mellon University, 1994"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Pol, J. Termination Proofs for Higher-Order Rewrite Systems, J. Heering, K. Meinke, B. Moller, T. Nipkow ed., Higher Order Algebra, Logic and Term Rewriting (HOA),Lecture Notes in Computer Science, vol 816, 1994, pages 305\u2013325","DOI":"10.1007\/3-540-58233-9_14"},{"key":"10_CR18","unstructured":"Prehofer, C. Solving Higher-Order Equations., Technical Report, Technische Universit\u00e4t M\u00fcnchen, 1994"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Rohwedder, E., Pfenning, F. Mode and Termination Analysis for Higher-Order Logic, to appear at the 1996 European Symposium on Programming (ESOP)","DOI":"10.1007\/3-540-61055-3_44"},{"key":"10_CR20","unstructured":"Salvesen, A. The Church-Rosser Property for Pure Systems with \u03b2\u03b7-Reduction. Technical Report, University of Oslo, 1992"},{"key":"10_CR21","unstructured":"Virga, R. Higher-Order Superposition for Dependent Types, Technical Report CMU-CS-95-150, Carnegie Mellon University, 1995 (http:\/\/www.cs.cmu.edu\/afs\/cs.cmu.edu\/user\/rvirga\/Web\/dep-rel.ps)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Wolfram, D.A Rewriting, and Equational Unification: the Higher-Order Cases Proceedings of the 4th International Conference on Rewriting Techniques and Applications (RTA), 1991, pages 25\u201336","DOI":"10.1007\/3-540-53904-2_83"}],"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_47.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:18:58Z","timestamp":1742599138000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}