{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:17:01Z","timestamp":1725560221326},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_5","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"54-68","source":"Crossref","is-referenced-by-count":6,"title":["Tabling for Higher-Order Logic Programming"],"prefix":"10.1007","author":[{"given":"Brigitte","family":"Pientka","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","first-page":"31","volume-title":"Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages","author":"M. Abadi","year":"1990","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e8vy, J.-J.: Explicit substitutions. In: Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, pp. 31\u201346. ACM, New York (1990)"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Felten, E.W.: Proof-carrying authentication. In: ACM Conference on Computer and Communications Security, pp. 52\u201362 (1999)","DOI":"10.1145\/319709.319718"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Appel, W., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000), January 2000, pp. 243\u2013253 (2000)","DOI":"10.1145\/325694.325727"},{"issue":"1","key":"5_CR4","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/227595.227597","volume":"43","author":"W. Chen","year":"1996","unstructured":"Chen, W., Warren, D.S.: Tabled evaluation with delaying for general logic programs. Journal of the ACM\u00a043(1), 20\u201374 (1996)","journal-title":"Journal of the ACM"},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1145\/604131.604149","volume-title":"30th ACM Symposiumn on Principles of Programming Languages (POPL)","author":"K. Crary","year":"2003","unstructured":"Crary, K.: Toward a foundational typed assembly language. In: 30th ACM Symposiumn on Principles of Programming Languages (POPL), New Orleans, Louisisana, pp. 198\u2013212. ACM-Press, New York (2003)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0056604","volume-title":"Principles of Declarative Programming","author":"B. Cui","year":"1998","unstructured":"Cui, B., Dong, Y., Du, X., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Roychoudhury, A., Smolka, S.A., Warren, D.S.: Logic programming and model checking. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol.\u00a01490, pp. 1\u201320. Springer, Heidelberg (1998)"},{"key":"5_CR7","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)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BFb0056605","volume-title":"International Symposium on Programming Language Implementation and Logic Programming (PLILP 1998)","author":"B. Demoen","year":"1998","unstructured":"Demoen, B., Sagonas, K.: CAT: The copying approach to tabling. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol.\u00a01490, pp. 21\u201336. Springer, Heidelberg (1998)"},{"issue":"1","key":"5_CR9","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":"5_CR10","series-title":"LNCAI","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/BFb0027414","volume-title":"Proceedings of the 6 t h Workshop on Theorem Proving with Analytic Tableaux and Related Methods","author":"J.M. Howe","year":"1997","unstructured":"Howe, J.M.: Two loop detection mechanisms: a comparison. In: TABLEAUX 1997. LNCAI, vol.\u00a01227, pp. 188\u2013200. Springer, Heidelberg (1997)"},{"key":"5_CR11","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":"5_CR12","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: Fifth International Logic Programming Conference, Seattle, Washington, August 1988, pp. 810\u2013827. MIT Press, Cambridge (1988)"},{"key":"5_CR13","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":"5_CR14","first-page":"93","volume-title":"Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS 1998)","author":"G. Necula","year":"1998","unstructured":"Necula, G., Lee, P.: Efficient representation and validation of logical proofs. In: Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS 1998), June 1998, pp. 93\u2013104. IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"5_CR15","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":"5_CR16","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1109\/LICS.1989.39186","volume-title":"Fourth Annual Symposium on Logic in Computer Science","author":"F. Pfenning","year":"1989","unstructured":"Pfenning, F.: Elf: A language for logic definition and verified meta-programming. In: Fourth Annual Symposium on Logic in Computer Science, Pacific Grove, California, June 1989, pp. 313\u2013322. IEEE Computer Society Press, Los Alamitos (1989)"},{"key":"5_CR17","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":"5_CR18","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 - A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"5_CR19","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":"5_CR20","unstructured":"Pientka, B.: Tabled higher-order logic programming. PhD thesis, Department of Computer Sciences, Carnegie Mellon University, CMU-CS-03-185 (December 2003)"},{"key":"5_CR21","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., Pfenning, 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":"5_CR22","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S0743-1066(98)10013-4","volume":"38","author":"I.V. Ramakrishnan","year":"1999","unstructured":"Ramakrishnan, I.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":"5_CR23","doi-asserted-by":"publisher","first-page":"1853","DOI":"10.1016\/B978-044450813-3\/50028-X","volume-title":"Handbook of Automated Reasoning","author":"I.V. Ramakrishnan","year":"2001","unstructured":"Ramakrishnan, I.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)"},{"issue":"3","key":"5_CR24","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1145\/291889.291897","volume":"20","author":"K. Sagonas","year":"1998","unstructured":"Sagonas, K., Swift, T.: An abstract machine for tabled execution of fixed-order stratified logic programs. ACM Transactions on Programming Languages and Systems\u00a020(3), 586\u2013634 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-16492-8_66","volume-title":"Third International Conference on Logic Programming","author":"H. Tamaki","year":"1986","unstructured":"Tamaki, H., Sato, T.: OLD resolution with tabulation. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol.\u00a0225, pp. 84\u201398. Springer, Heidelberg (1986)"},{"key":"5_CR26","unstructured":"Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, Available as Technical Report CMU-CS-99-167 (Sep. 1999)"},{"key":"5_CR27","unstructured":"Warren, D.S.: Programming in tabled logic programming. draft (1999), available from \n                  \n                    http:\/\/www.cs.sunysb.edu\/~warren\/xsbbook\/book.html"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:09:15Z","timestamp":1605643755000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11532231_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}