{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T04:17:04Z","timestamp":1748405824143,"version":"3.41.0"},"publisher-location":"Singapore","reference-count":28,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819789429"},{"type":"electronic","value":"9789819789436"}],"license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-97-8943-6_3","type":"book-chapter","created":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T08:45:29Z","timestamp":1730105129000},"page":"42-62","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Generic Reasoning of the Locally Nameless Representation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-2238-0990","authenticated-orcid":false,"given":"Yicheng","family":"Ni","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3990-2418","authenticated-orcid":false,"given":"Yuting","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,28]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Allais, G., Atkey, R., Chapman, J., McBride, C., McKinna, J.: A type and scope safe universe of syntaxes with binding: their semantics and proofs. In: Proceedings of the ACM on Programming Languages 2(ICFP) (2018). https:\/\/doi.org\/10.1145\/3236785","DOI":"10.1145\/3236785"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Amin, N., Rompf, T.: Type soundness proofs with definitional interpreters. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 666\u2013679. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3009837.3009866","DOI":"10.1145\/3009837.3009866"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 3\u201315. ACM, New York (2008). https:\/\/doi.org\/10.1145\/1328438.1328443","DOI":"10.1145\/1328438.1328443"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: the POPLMARK challenge. In: Theorem Proving in Higher Order Logics, pp. 50\u201365. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/115418","DOI":"10.1007\/115418"},{"key":"3_CR5","unstructured":"Aydemir, B.E., Weirich, S.: Lngen: Tool support for locally nameless representations (2010). https:\/\/api.semanticscholar.org\/CorpusID:2649490"},{"issue":"2","key":"3_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/issn.1972-5787\/4650","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formalized Reasoning 7(2), 1\u201389 (2014). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"J. Formalized Reasoning"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. 33(2) (2011). https:\/\/doi.org\/10.1145\/1890028.1890031","DOI":"10.1145\/1890028.1890031"},{"issue":"5","key":"3_CR8","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.entcs.2007.01.018","volume":"174","author":"S Berghofer","year":"2007","unstructured":"Berghofer, S., Urban, C.: A head-to-head comparison of de Bruijn indices and names. Electron. Notes Theor. Comput. Sci. 174(5), 53\u201367 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2007.01.018","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"49","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reason. 49, 363\u2013408 (2012). https:\/\/doi.org\/10.1007\/s10817-011-9225-2","journal-title":"J. Autom. Reason."},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, pp. 143\u2013156. ACM, New York (2008). https:\/\/doi.org\/10.1145\/1411204.1411226","DOI":"10.1145\/1411204.1411226"},{"issue":"5","key":"3_CR11","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"N de Bruijn","year":"1972","unstructured":"de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75(5), 381\u2013392 (1972). https:\/\/doi.org\/10.1016\/1385-7258(72)90034-0","journal-title":"Indagationes Mathematicae (Proceedings)"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in coq. In: International Conference on Typed Lambda Calculi and Applications, pp. 124\u2013138. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0014049","DOI":"10.1007\/BFb0014049"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Fiore, M.: Second-order and dependently-sorted abstract syntax. In: Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science, pp. 57\u201368. IEEE, New York (2008). https:\/\/doi.org\/10.1109\/LICS.2008.38","DOI":"10.1109\/LICS.2008.38"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Fiore, M., Szamozvancev, D.: Formal metatheory of second-order abstract syntax. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498715","DOI":"10.1145\/3498715"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Harper, R.: Practical Foundations for Programming Languages, pp. 455\u2013474. Cambridge University Press (2016). http:\/\/www.cs.cmu.edu\/~rwh\/pfpl.html","DOI":"10.1017\/CBO9781316576892"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"McKinna, J., Pollack, R.: Pure type systems formalized. In: Typed Lambda Calculi and Applications: International Conference on Typed Lambda Calculi and Applications, pp. 289\u2013305. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0037113","DOI":"10.1007\/BFb0037113"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Miller, D.: Abstract syntax for variable binders: an overview. In: Proceedings of the First International Conference on Computational Logic, pp. 239\u2013253. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44957-4_16","DOI":"10.1007\/3-540-44957-4_16"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, pp. 199\u2013208. ACM, New York (1988). https:\/\/doi.org\/10.1145\/53990.54010","DOI":"10.1145\/53990.54010"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf\u2014a meta-logical framework for deductive systems. In: Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, pp. 202\u2013206. CADE-16, Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_14","DOI":"10.1007\/3-540-48660-7_14"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Pientka, B., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (system description). In: Giesl, J., H\u00e4hnle, R. (eds.) Automated Reasoning, pp. 15\u201321. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_2","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Pitts, A.M.: Locally nameless sets. Proc. Program. Lang. 7(POPL) (2023). https:\/\/doi.org\/10.1145\/3571210","DOI":"10.1145\/3571210"},{"issue":"3","key":"3_CR22","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G Plotkin","year":"1977","unstructured":"Plotkin, G.: Lcf considered as a programming language. Theoret. Comput. Sci. 5(3), 223\u2013255 (1977). https:\/\/doi.org\/10.1016\/0304-3975(77)90044-5","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. In: Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, pp. 89\u2013102. ACM, New York (2010). https:\/\/doi.org\/10.1145\/1708016.1708028","DOI":"10.1145\/1708016.1708028"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Sch\u00e4fer, S., Tebbi, T., Smolka, G.: Autosubst: reasoning with de Bruijn terms and parallel substitutions. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving, pp. 359\u2013374. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_24","DOI":"10.1007\/978-3-319-22102-1_24"},{"issue":"1","key":"3_CR25","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1145\/1291220.1291155","volume":"20","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., et al.: Ott: effective tool support for the working semanticist. J. Funct. Program. 20(1), 71\u2013122 (2010). https:\/\/doi.org\/10.1145\/1291220.1291155","journal-title":"J. Funct. Program."},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Stark, K., Sch\u00e4fer, S., Kaiser, J.: Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 166\u2013180. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3293880.3294101","DOI":"10.1145\/3293880.3294101"},{"issue":"3","key":"3_CR27","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-011-9230-5","volume":"49","author":"J Vouillon","year":"2012","unstructured":"Vouillon, J.: A solution to the POPLMARK challenge based on de Bruijn indices. J. Autom. Reason. 49(3), 327\u2013362 (2012). https:\/\/doi.org\/10.1007\/s10817-011-9230-5","journal-title":"J. Autom. Reason."},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Weirich, S., Yorgey, B.A., Sheard, T.: Binders unbound. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, pp. 333\u2013345. ACM, New York (2011). https:\/\/doi.org\/10.1145\/2034773.2034818","DOI":"10.1145\/2034773.2034818"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-97-8943-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T16:52:35Z","timestamp":1748364755000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-97-8943-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"ISBN":["9789819789429","9789819789436"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-981-97-8943-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,28]]},"assertion":[{"value":"28 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}