{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:54Z","timestamp":1774837854805,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,9,19]],"date-time":"2011-09-19T00:00:00Z","timestamp":1316390400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2011,9,19]]},"DOI":"10.1145\/2034773.2034818","type":"proceedings-article","created":{"date-parts":[[2011,9,20]],"date-time":"2011-09-20T09:50:16Z","timestamp":1316512216000},"page":"333-345","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Binders unbound"],"prefix":"10.1145","author":[{"given":"Stephanie","family":"Weirich","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brent A.","family":"Yorgey","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Sheard","sequence":"additional","affiliation":[{"name":"Portland State University, Portland, OR, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,9,19]]},"reference":[{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_3_2_2_3_1","unstructured":"C. Calv\u00e8s. A Haskell nominal toolkit. http:\/\/www.inf.kcl.ac.uk\/pg\/calves\/hnt\/ Jan. 2009.  C. Calv\u00e8s. A Haskell nominal toolkit. http:\/\/www.inf.kcl.ac.uk\/pg\/calves\/hnt\/ Jan. 2009."},{"key":"e_1_3_2_2_4_1","volume-title":"Special Issue on the POPLmark Challenge","author":"Chargu\u00e9raud A.","year":"2011","unstructured":"A. Chargu\u00e9raud . The locally nameless representation. Journal of Automated Reasoning , Special Issue on the POPLmark Challenge , 2011 . To appear. A. Chargu\u00e9raud. The locally nameless representation. Journal of Automated Reasoning, Special Issue on the POPLmark Challenge, 2011. To appear."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088454.1088459"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086389"},{"key":"e_1_3_2_2_7_1","volume-title":"Proceedings of the Third International Workshop on Reduction Strategies in Rewriting and Programming","author":"Cirstea H.","year":"2003","unstructured":"H. Cirstea , C. Kirchner , L. Liquori , and B. Wack . Rewrite strategies in the rewriting calculus. In B. Gramlich and S. Lucas, editors , Proceedings of the Third International Workshop on Reduction Strategies in Rewriting and Programming , Valencia, Spain , June 2003 . Electronic Notes in Theoretical Computer Science. H. Cirstea, C. Kirchner, L. Liquori, and B. Wack. Rewrite strategies in the rewriting calculus. In B. Gramlich and S. Lucas, editors, Proceedings of the Third International Workshop on Reduction Strategies in Rewriting and Programming, Valencia, Spain, June 2003. Electronic Notes in Theoretical Computer Science."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90066-B"},{"key":"e_1_3_2_2_10_1","volume-title":"North-Holland","author":"Gentzen G.","year":"1969","unstructured":"G. Gentzen . The Collected Papers of Gerhard Gentzen . North-Holland , 1969 . Edited by Mandred Szabo. G. Gentzen. The Collected Papers of Gerhard Gentzen. North-Holland, 1969. Edited by Mandred Szabo."},{"key":"e_1_3_2_2_11_1","series-title":"Lecture Notes in Computer Science","first-page":"414","volume-title":"Higher-order Logic Theorem Proving And Its Applications","author":"Gordon A. D.","year":"1993","unstructured":"A. D. Gordon . A mechanisation of name-carrying syntax up to alpha-conversion . In J. Joyce and C. Seger, editors, Higher-order Logic Theorem Proving And Its Applications , Proceedings, 1993 , volume 780 of Lecture Notes in Computer Science , pages 414 -- 426 . Springer , 1994. A. D. Gordon. A mechanisation of name-carrying syntax up to alpha-conversion. In J. Joyce and C. Seger, editors, Higher-order Logic Theorem Proving And Its Applications, Proceedings, 1993, volume 780 of Lecture Notes in Computer Science, pages 414--426. Springer, 1994."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792884"},{"key":"e_1_3_2_2_13_1","volume-title":"USA","author":"Kleene S.","year":"1952","unstructured":"S. Kleene . Introduction to Metamathematics. ban Nostrand Rheinhold, Princeton , USA , 1952 . S. Kleene. Introduction to Metamathematics. ban Nostrand Rheinhold, Princeton, USA, 1952."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086391"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_3_2_2_17_1","volume-title":"Sweden","author":"Norell U.","year":"2007","unstructured":"U. Norell . Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg , Sweden , September 2007 . U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg, Sweden, September 2007."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.039"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.44"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863575"},{"key":"e_1_3_2_2_24_1","volume-title":"Almquist and Wiksell","author":"Prawitz D.","year":"1965","unstructured":"D. Prawitz . Natural Deduction : Proof Theoretical Study . Almquist and Wiksell , Stockholm , 1965 . D. Prawitz. Natural Deduction: Proof Theoretical Study. Almquist and Wiksell, Stockholm, 1965."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543134.1411301"},{"key":"e_1_3_2_2_26_1","volume-title":"Oct.","author":"Sarkar S.","year":"2007","unstructured":"S. Sarkar , P. Sewell , and F. Zappa Nardelli . Binding and substitution. www.cl.cam.ac.uk\/~pes20\/ott\/bind-doc.pdf , Oct. 2007 . S. Sarkar, P. Sewell, and F. Zappa Nardelli. Binding and substitution. www.cl.cam.ac.uk\/~pes20\/ott\/bind-doc.pdf, Oct. 2007."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289460"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636528"},{"key":"e_1_3_2_2_30_1","volume-title":"Fresh Objective Caml User Manual","author":"Shinwell M.","year":"2005","unstructured":"M. Shinwell and A. Pitts . Fresh Objective Caml User Manual . Cambridge University Computer Laboratory , Feb. 2005 . M. Shinwell and A. Pitts. Fresh Objective Caml User Manual. Cambridge University Computer Laboratory, Feb. 2005."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944729"},{"key":"e_1_3_2_2_32_1","volume-title":"How to prove false using the variable convention. Appears as a poster at TTVSI, 1 page, mar","author":"Urban C.","year":"2008","unstructured":"C. Urban . How to prove false using the variable convention. Appears as a poster at TTVSI, 1 page, mar 2008 . C. Urban. How to prove false using the variable convention. Appears as a poster at TTVSI, 1 page, mar 2008."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987236"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159844"},{"key":"e_1_3_2_2_36_1","volume-title":"A locally-nameless backend for Ott. moscova.inria.fr\/~zappa\/projects\/ln_ott\/","author":"Nardelli F. Zappa","year":"2009","unstructured":"F. Zappa Nardelli . A locally-nameless backend for Ott. moscova.inria.fr\/~zappa\/projects\/ln_ott\/ , 2009 . F. Zappa Nardelli. A locally-nameless backend for Ott. moscova.inria.fr\/~zappa\/projects\/ln_ott\/, 2009."}],"event":{"name":"ICFP '11: ACM SIGPLAN International Conference on Functional Programming","location":"Tokyo Japan","acronym":"ICFP '11","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 16th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2034773.2034818","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2034773.2034818","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:39Z","timestamp":1750225719000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2034773.2034818"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,19]]},"references-count":34,"alternative-id":["10.1145\/2034773.2034818","10.1145\/2034773"],"URL":"https:\/\/doi.org\/10.1145\/2034773.2034818","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2034574.2034818","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2011,9,19]]},"assertion":[{"value":"2011-09-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}