{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:02:18Z","timestamp":1770282138387,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540406648","type":"print"},{"value":"9783540451303","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_16","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T15:27:09Z","timestamp":1150730829000},"page":"238-252","source":"Crossref","is-referenced-by-count":7,"title":["Extending Higher-Order Unification to Support Proof Irrelevance"],"prefix":"10.1007","author":[{"given":"Jason","family":"Reed","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"16_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 Press, New York (1990)"},{"key":"16_CR2","unstructured":"Crary, K., Sarkar, S.: A metalogical approach to foundational certified code. Technical Report CMU-CS-03-108, Carnegie Mellon University (January 2003)"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1109\/LICS.1995.523271","volume-title":"Proceedings of the Tenth Annual Symposium on Logic in Computer Science","author":"G. Dowek","year":"1995","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. In: Kozen, D. (ed.) Proceedings of the Tenth Annual Symposium on Logic in Computer Science, San Diego, California, June 1995, pp. 366\u2013374. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"16_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)"},{"issue":"1","key":"16_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"},{"issue":"4","key":"16_CR6","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation\u00a01(4), 497\u2013536 (1991)","journal-title":"Journal of Logic and Computation"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/LICS.2001.932499","volume-title":"Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS 2001)","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: Halpern, J. (ed.) Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS 2001), Boston, Massachusetts, June 2001, pp. 221\u2013230. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Symposium on Language Design and Implementation, Atlanta, Georgia, June 1998, pp. 199\u2013208 (1998)","DOI":"10.1145\/960116.54010"},{"key":"16_CR9","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)"},{"key":"16_CR10","unstructured":"Reed, J.: Higher-order pattern unification and proof irrelevance. Appears in TPHOLs 2002 Track B proceedings, NASA tech report CP-2002-211736 (2002)"},{"key":"16_CR11","unstructured":"Reed, J.: Proof irrelevance and strict definitions in a logical framework. Technical Report CMU-CS-02-153, Carnegie Mellon University (2002)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-61055-3_44","volume-title":"Programming Languages and Systems - ESOP \u201996","author":"E. Rohwedder","year":"1996","unstructured":"Rohwedder, E., Pfenning, F.: Mode and termination checking for higher-order logic programs. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol.\u00a01058, pp. 296\u2013310. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10930755_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,28]],"date-time":"2021-07-28T14:15:26Z","timestamp":1627481726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/10930755_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}