{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T06:40:03Z","timestamp":1736577603736,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_32","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"362-376","source":"Crossref","is-referenced-by-count":2,"title":["Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach"],"prefix":"10.1007","author":[{"given":"Brigitte","family":"Pientka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1109\/LICS.2001.932501","volume-title":"Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS 2001)","author":"A. Appel","year":"2001","unstructured":"Appel, A.: Foundational proof-carrying code. In: Halpern, J. (ed.) Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS 2001), pp. 247\u2013256. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Aydemir","year":"2005","unstructured":"Aydemir, B., et al.: Mechanized metatheory for the masses: The poplmark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"key":"32_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-540-45085-6_9","volume-title":"Automated Deduction \u2013 CADE-19","author":"K. Crary","year":"2003","unstructured":"Crary, K., Sarkar, S.: Foundational certified code in a metalogical framework. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 106\u2013120. Springer, Heidelberg (2003)"},{"key":"32_CR4","first-page":"259","volume-title":"Proceedings of the Joint International Conference and Symposium on Logic Programming","author":"G. Dowek","year":"1996","unstructured":"Dowek, G., Hardin, T., Kirchner, C., Pfenning, F.: Unification via explicit substitutions: The case of higher-order patterns. In: Maher, M. (ed.) Proceedings of the Joint International Conference and Symposium on Logic Programming, Bonn, Germany, September 1996, pp. 259\u2013273. MIT Press, Cambridge (1996)"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Hannan, J., Pfenning, F.: Compiler verification in LF. In: Scedrov, A. (ed.) Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, June 1992, pp. 407\u2013418 (1992)","DOI":"10.1109\/LICS.1992.185552"},{"issue":"1","key":"32_CR6","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":"32_CR7","unstructured":"Michaylov, S., Pfenning, F.: An empirical study of the runtime behavior of higher-order logic programs. In: Miller, D. (ed.) Proceedings of the Workshop on the \u03bbProlog Programming Language, Philadelphia, Pennsylvania, July 1992, pp. 257\u2013271. University of Pennsylvania (1992)"},{"key":"32_CR8","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":"32_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/11591191_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Nadathur","year":"2005","unstructured":"Nadathur, G., Qi, X.: Optimizing the runtime processing of types in polymorphic logic programming languages. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 110\u2013124. Springer, Heidelberg (2005)"},{"key":"32_CR10","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: A contextual modal type theory (2005)"},{"key":"32_CR11","first-page":"93","volume-title":"Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS 1998)","author":"G.C. Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: Efficient representation and validation of logical proofs. In: Pratt, V. (ed.) Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS 1998), Indianapolis, Indiana, June 1998, pp. 93\u2013104. IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"32_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":"32_CR13","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/B978-044450813-3\/50019-9","volume-title":"Handbook of automated reasoning","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of automated reasoning, Amsterdam, The Netherlands, pp. 1063\u20131147. Elsevier Science Publishers B. V, Amsterdam (2001)"},{"key":"32_CR14","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 meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"32_CR15","unstructured":"Pientka, B.: Tabled higher-order logic programming. PhD thesis, Department of Computer Sciences, Carnegie Mellon University, CMU-CS-03-185 (December, 2003)"},{"key":"32_CR16","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)"},{"key":"32_CR17","unstructured":"Reed, J.: Redundancy Elimination for LF. In: Schuermann, C. (ed.) Fourth Workshop on Logical Frameworks and Meta-languages( LFM 2004), Cork, Ireland (July 2004)"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University (2002)","DOI":"10.21236\/ADA418517"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T06:09:10Z","timestamp":1736575750000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11814771_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}