{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:56:37Z","timestamp":1743126997821,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005893"},{"type":"electronic","value":"9783642005909"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00590-9_4","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T08:05:58Z","timestamp":1238141158000},"page":"47-61","source":"Crossref","is-referenced-by-count":3,"title":["Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming"],"prefix":"10.1007","author":[{"given":"Matthew R.","family":"Lakin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew M.","family":"Pitts","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (1984); revised edition"},{"key":"4_CR2","unstructured":"Byrd, W.E., Friedman, D.P.: alphaKanren: A fresh name in nominal logic programming. In: Proc. 2007 Workshop on Scheme and Functional Programming, number DIUL-RT-0701 in Universit\u00e9 Laval Technical Reports, pp. 79\u201390 (2007)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-69937-8_11","volume-title":"Logic, Language, Information and Computation","author":"C. Calv\u00e8s","year":"2008","unstructured":"Calv\u00e8s, C., Fern\u00e1ndez, M.: Nominal matching and alpha-equivalence. In: Hodges, W., de Queiroz, R. (eds.) Logic, Language, Information and Computation. LNCS, vol.\u00a05110, pp. 111\u2013122. Springer, Heidelberg (2008)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-27836-8_30","volume-title":"Automata, Languages and Programming","author":"J. Cheney","year":"2004","unstructured":"Cheney, J.: The complexity of equivariant unification. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 332\u2013344. Springer, Heidelberg (2004)"},{"key":"4_CR5","unstructured":"Cheney, J.: Nominal Logic Programming. PhD thesis, Cornell Univ. (2004)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-32033-3_7","volume-title":"Term Rewriting and Applications","author":"J. Cheney","year":"2005","unstructured":"Cheney, J.: Equivariant unification. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 74\u201389. Springer, Heidelberg (2005)"},{"issue":"5","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1387673.1387675","volume":"30","author":"J. Cheney","year":"2008","unstructured":"Cheney, J., Urban, C.: Nominal logic programming. Trans. Prog. Lang. and Systems\u00a030(5), 1\u201347 (2008)","journal-title":"Trans. Prog. Lang. and Systems"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math.\u00a034, 381\u2013392 (1972)","journal-title":"Indag. Math."},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M. Felleisen","year":"1992","unstructured":"Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoret. Comput. Science\u00a0103, 235\u2013271 (1992)","journal-title":"Theoret. Comput. Science"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/173262.155113","volume":"28","author":"C. Flanagan","year":"1993","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. SIGPLAN Not.\u00a028, 237\u2013247 (1993)","journal-title":"SIGPLAN Not."},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1016\/j.jal.2005.10.012","volume":"5","author":"M.J. Gabbay","year":"2007","unstructured":"Gabbay, M.J.: Fresh logic: Proof-theory and semantics for FM and nominal techniques. J. Appl. Logic\u00a05, 356\u2013387 (2007)","journal-title":"J. Appl. Logic"},{"key":"4_CR12","unstructured":"Gordon, A.D.: Operational equivalences for untyped and polymorphic object calculi. In: Gordon and Pitts [13], pp. 9\u201354"},{"volume-title":"Higher Order Operational Techniques in Semantics","year":"1998","key":"4_CR13","unstructured":"Gordon, A.D., Pitts, A.M. (eds.): Higher Order Operational Techniques in Semantics. Cambridge University Press, Cambridge (1998)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-540-74610-2_5","volume-title":"Logic Programming","author":"M. Hanus","year":"2007","unstructured":"Hanus, M.: Multi-paradigm declarative languages. In: Dahl, V., Niemel\u00e4, I. (eds.) ICLP 2007. LNCS, vol.\u00a04670, pp. 45\u201375. Springer, Heidelberg (2007)"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0743-1066(98)10002-X","volume":"37","author":"J. Jaffar","year":"1998","unstructured":"Jaffar, J., Maher, M., Marriott, K., Stuckey, P.: Semantics of constraint logic programming. J. Logic Programming\u00a037, 1\u201346 (1998)","journal-title":"J. Logic Programming"},{"key":"4_CR16","unstructured":"Lakin, M.R., Pitts, A.M.: A metalanguage for structural operational semantics. In: Trends in Functional Programming, vol.\u00a08, pp. 19\u201335. Intellect (2008)"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Lassen, S.B.: Relational reasoning about contexts. In: Gordon and Pitts [13], pp. 91\u2013135","DOI":"10.7146\/brics.v4i24.18950"},{"key":"4_CR18","first-page":"241","volume-title":"LICS 2008 Proceedings","author":"D.R. Licata","year":"2008","unstructured":"Licata, D.R., Zeilberger, N., Harper, R.: Focusing on binding and computation. In: LICS 2008 Proceedings, pp. 241\u2013252. IEEE Computer Society, Los Alamitos (2008)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/3-540-44957-4_16","volume-title":"Computational Logic - CL 2000","author":"D.A. Miller","year":"2000","unstructured":"Miller, D.A.: Abstract syntax for variable binders: An overview. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS, vol.\u00a01861, pp. 239\u2013253. Springer, Heidelberg (2000)"},{"key":"4_CR20","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"R. Milner","year":"1997","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)"},{"key":"4_CR21","first-page":"199","volume-title":"PLDI 1988 Proceedings","author":"F. Pfenning","year":"1988","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI 1988 Proceedings, pp. 199\u2013208. ACM Press, New York (1988)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-45699-6_8","volume-title":"Applied Semantics","author":"A.M. Pitts","year":"2002","unstructured":"Pitts, A.M.: Operational semantics and program equivalence. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol.\u00a02395, pp. 378\u2013412. Springer, Heidelberg (2002)"},{"key":"4_CR23","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. and Comput.\u00a0186, 165\u2013193 (2003)","journal-title":"Inf. and Comput."},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1145\/1147954.1147961","volume":"53","author":"A.M. Pitts","year":"2006","unstructured":"Pitts, A.M.: Alpha-structural recursion and induction. J. ACM\u00a053, 459\u2013506 (2006)","journal-title":"J. ACM"},{"key":"4_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-4(1:4)2008","volume":"4","author":"A.M. Pitts","year":"2008","unstructured":"Pitts, A.M., Shinwell, M.R.: Generative unbinding of names. Logical Methods in Comput. Science\u00a04, 1\u201333 (2008)","journal-title":"Logical Methods in Comput. Science"},{"key":"4_CR26","first-page":"263","volume-title":"ICFP 2003 Proceedings","author":"M.R. Shinwell","year":"2003","unstructured":"Shinwell, M.R., Pitts, A.M., Gabbay, M.J.: FreshML: Programming with binders made simple. In: ICFP 2003 Proceedings, pp. 263\u2013274. ACM Press, New York (2003)"},{"key":"4_CR27","series-title":"Electr. Notes in Theoret. Comp. Science","first-page":"16","volume-title":"WFLP 2003 Proceedings","author":"A. Tolmach","year":"2003","unstructured":"Tolmach, A., Antoy, S.: A monadic semantics for core Curry. In: WFLP 2003 Proceedings. Electr. Notes in Theoret. Comp. Science, vol.\u00a086(3), pp. 16\u201334. Elsevier, Amsterdam (2003)"},{"key":"4_CR28","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.tcs.2004.06.016","volume":"323","author":"C. Urban","year":"2004","unstructured":"Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoret. Comp. Science\u00a0323, 473\u2013497 (2004)","journal-title":"Theoret. Comp. Science"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00590-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,7]],"date-time":"2019-03-07T02:23:46Z","timestamp":1551925426000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00590-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005893","9783642005909"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00590-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}