{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:34:56Z","timestamp":1725561296519},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540206422"},{"type":"electronic","value":"9783540245995"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-24599-5_26","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T04:53:55Z","timestamp":1280379235000},"page":"377-391","source":"Crossref","is-referenced-by-count":5,"title":["Higher-Order Substitution Tree Indexing"],"prefix":"10.1007","author":[{"given":"Brigitte","family":"Pientka","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1145\/351240.351259","volume-title":"Proceedings of the International Conference on Functional Programming (ICFP 2000)","author":"R. Davies","year":"2000","unstructured":"Davies, R., Pfenning, F.: Intersection types and computational effects. In: Proceedings of the International Conference on Functional Programming (ICFP 2000), Montreal, Canada, pp. 198\u2013208. ACM Press, New York (2000)"},{"issue":"6","key":"26_CR2","first-page":"528","volume":"18","author":"S. Dawson","year":"1995","unstructured":"Dawson, S., Ramakrishnan, C.R., Skiena, S., Swift, T.: Principles and practice of unification factoring. ACM Transactions on Programming Languages and Systems\u00a018(6), 528\u2013563 (1995)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/3-540-59200-8_52","volume-title":"Rewriting Techniques and Applications","author":"P. Graf","year":"1995","unstructured":"Graf, P.: Substitution tree indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914, pp. 117\u2013131. Springer, Heidelberg (1995)"},{"issue":"1","key":"26_CR4","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S0956796899003330","volume":"9","author":"M. Hanus","year":"1999","unstructured":"Hanus, M., Prehofer, C.: Higher-order narrowing with definitional trees. Journal of Functional Programming\u00a09(1), 33\u201375 (1999)","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"26_CR5","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"26_CR6","unstructured":"Klein, L.: Indexing f\u00fcr Terme h\u00f6herer Stufe. Diplomarbeit, FB 14, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (1997)"},{"key":"26_CR7","first-page":"255","volume-title":"Eighth International Logic Programming Conference","author":"D. Miller","year":"1991","unstructured":"Miller, D.: Unification of simply typed lambda-terms as logic programming. In: Eighth International Logic Programming Conference, Paris, France, June 1991, pp. 255\u2013269. MIT Press, Cambridge (1991)"},{"key":"26_CR8","first-page":"810","volume-title":"Fifth International Logic Programming Conference","author":"G. Nadathur","year":"1988","unstructured":"Nadathur, G., Miller, D.: An overview of \u03bbProlog. In: Bowen, K.A., Kowalski, R.A. (eds.) Fifth International Logic Programming Conference, Seattle, Washington, August 1988, pp. 810\u2013827. MIT Press, Cambridge (1988)"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Pientka, B., Pfenning, F.: A modal foundation for meta-variables. In: 2nd ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with variable binding (Merlin), Uppsala, Sweden (August 2003) (to appear)","DOI":"10.1145\/976571.976582"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Necula, G., Rahul, S.: Oracle-based checking of untrusted software. In: 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 142\u2013154 (2001)","DOI":"10.1145\/360204.360216"},{"key":"26_CR11","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"L.C. Paulson","year":"1986","unstructured":"Paulson, L.C.: Natural deduction as higher-order resolution. Journal of Logic Programming\u00a03, 237\u2013258 (1986)","journal-title":"Journal of Logic Programming"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Unification and anti-unification in the Calculus of Constructions. In: Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, July 1991, pp. 74\u201385 (1991)","DOI":"10.1109\/LICS.1991.151632"},{"key":"26_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2014 a metalogical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Pientka, B.: Memoization-based proof search in LF: an experimental evaluation of a prototype. In: Third International Workshop on Logical Frameworks and Meta-Languages (LFM 2002), Copenhagen, Denmark. Electronic Notes in Theoretical Computer Science, ENTCS (2002)","DOI":"10.1016\/S1571-0661(04)80509-7"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-45619-8_19","volume-title":"Logic Programming","author":"B. Pientka","year":"2002","unstructured":"Pientka, B.: A proof-theoretic foundation for tabled higher-order logic programming. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol.\u00a02401, pp. 271\u2013286. Springer, Heidelberg (2002)"},{"key":"26_CR16","unstructured":"Pientka, B.: Tabled higher-order logic programming. PhD thesis, Department of Computer Sciences, Carnegie Mellon University (2003) (forthcoming)"},{"key":"26_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-540-45085-6_40","volume-title":"Automated Deduction \u2013 CADE-19","author":"B. Pientka","year":"2003","unstructured":"Pientka, B., Pfennning, F.: Optimizing higher-order pattern unification. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 473\u2013487. Springer, Heidelberg (2003)"},{"issue":"1","key":"26_CR18","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S0743-1066(98)10013-4","volume":"38","author":"V. Ramakrishnan","year":"1999","unstructured":"Ramakrishnan, V., Rao, P., Sagonas, K., Swift, T., Warren, D.: Efficient access mechanisms for tabled logic programs. Journal of Logic Programming\u00a038(1), 31\u201354 (1999)","journal-title":"Journal of Logic Programming"},{"key":"26_CR19","doi-asserted-by":"publisher","first-page":"1853","DOI":"10.1016\/B978-044450813-3\/50028-X","volume-title":"Handbook of Automated Reasoning","author":"V. Ramakrishnan","year":"2001","unstructured":"Ramakrishnan, V., Sekar, R., Voronkov, A.: Term indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, pp. 1853\u20131962. Elsevier Science Publishers B.V., Amsterdam (2001)"},{"key":"26_CR20","unstructured":"Warren, D.S.: Programming in tabled logic programming (1999), draft available from http:\/\/www.cs.sunysb.edu\/~warren\/xsbbook\/book.html"}],"container-title":["Lecture Notes in Computer Science","Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24599-5_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:55:15Z","timestamp":1559332515000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24599-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540206422","9783540245995"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24599-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}