{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:12:49Z","timestamp":1725585169281},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642216909"},{"type":"electronic","value":"9783642216916"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21691-6_5","type":"book-chapter","created":{"date-parts":[[2011,6,11]],"date-time":"2011-06-11T01:31:26Z","timestamp":1307755886000},"page":"10-26","source":"Crossref","is-referenced-by-count":10,"title":["Higher-Order Dynamic Pattern Unification for Dependent Types and Records"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"5_CR1","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1093\/logcom\/13.5.639","volume":"13","author":"I. Cervesato","year":"2003","unstructured":"Cervesato, I., Pfenning, F.: A linear spine calculus. Journal of Logic and Computation\u00a013(5), 639\u2013688 (2003)","journal-title":"Journal of Logic and Computation"},{"key":"5_CR2","first-page":"259","volume-title":"Joint International Conference 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: Joint International Conference Logic Programming, pp. 259\u2013273. MIT Press, Cambridge (1996)"},{"issue":"1-2","key":"5_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00141-2","volume":"206","author":"D. Duggan","year":"1998","unstructured":"Duggan, D.: Unification with extended patterns. Theoretical Computer Science\u00a0206(1-2), 1\u201350 (1998)","journal-title":"Theoretical Computer Science"},{"key":"5_CR4","unstructured":"Elliott, C.: Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University (1990)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-61464-8_64","volume-title":"Rewriting Techniques and Applications","author":"R. Fettig","year":"1996","unstructured":"Fettig, R., L\u00f6chner, B.: Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 347\u2013361. Springer, Heidelberg (1996)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-540-31982-5_26","volume-title":"Foundations of Software Science and Computational Structures","author":"H. Goguen","year":"2005","unstructured":"Goguen, H.: Justifying algorithms for \u03b2\u03b7 conversion. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 410\u2013424. Springer, Heidelberg (2005)"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science\u00a013, 225\u2013230 (1981)","journal-title":"Theoretical Computer Science"},{"key":"5_CR8","first-page":"1","volume-title":"ACM SIGPLAN Workshop on Genetic Programming (WGP 2010)","author":"C. McBride","year":"2010","unstructured":"McBride, C.: Outrageous but meaningful coincidences: Dependent type-safe syntax and evaluation. In: ACM SIGPLAN Workshop on Genetic Programming (WGP 2010), pp. 1\u201312. ACM, New York (2010)"},{"key":"5_CR9","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, pp. 255\u2013269. MIT Press, Cambridge (1991)"},{"issue":"3","key":"5_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1352582.1352591","volume":"9","author":"A. Nanevski","year":"2008","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic\u00a09(3), 1\u201349 (2008)","journal-title":"ACM Transactions on Computational Logic"},{"key":"5_CR11","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Technical Report 33D (2007)"},{"key":"5_CR12","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_CR13","unstructured":"Pientka, B.: Tabled higher-order logic programming. PhD thesis, Department of Computer Science, Carnegie Mellon University, CMU-CS-03-185 (2003)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-14203-1_2","volume-title":"Automated Reasoning","author":"B. Pientka","year":"2010","unstructured":"Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (System Description). In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 15\u201321. Springer, Heidelberg (2010)"},{"key":"5_CR15","series-title":"ENTCS","first-page":"135","volume-title":"International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008)","author":"A. Poswolsky","year":"2009","unstructured":"Poswolsky, A., Sch\u00fcrmann, C.: System description: Delphin\u2014a functional programming language for deductive systems. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008). ENTCS, vol.\u00a0228, pp. 135\u2013141. Elsevier, Amsterdam (2009)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Reed, J.: Higher-order constraint simplification in dependent type theory. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009 (2009)","DOI":"10.1145\/1577824.1577832"},{"key":"5_CR17","unstructured":"Reed, J.: A Hybrid Logical Framework. PhD thesis, School of Computer Science, Carnegie Mellon University (2009)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Schack-Nielson, A., Sch\u00fcrmann, C.: Pattern unification for the lambda calculus with linear and affine types. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2010). EPTCS, vol.\u00a034, pp. 101\u2013116 (2010)","DOI":"10.4204\/EPTCS.34.9"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh (2003)","DOI":"10.21236\/ADA418517"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21691-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T12:57:30Z","timestamp":1560257850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21691-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642216909","9783642216916"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21691-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}