{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:20:50Z","timestamp":1759638050355},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,4,16]],"date-time":"2013-04-16T00:00:00Z","timestamp":1366070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,2]]},"DOI":"10.1007\/s10817-013-9287-4","type":"journal-article","created":{"date-parts":[[2013,4,15]],"date-time":"2013-04-15T02:09:54Z","timestamp":1365991794000},"page":"215-239","source":"Crossref","is-referenced-by-count":3,"title":["Mechanizing Metatheory Without Typing Contexts"],"prefix":"10.1007","volume":"52","author":[{"given":"Jonghyun","family":"Park","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeongbong","family":"Seo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sungwoo","family":"Park","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gyesik","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,4,16]]},"reference":[{"key":"9287_CR1","doi-asserted-by":"crossref","unstructured":"Aydemir, B., 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: Hurd, J., Melham, T.F. (eds.) Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), pp. 50\u201365. Springer (2005)","DOI":"10.1007\/11541868_4"},{"key":"9287_CR2","doi-asserted-by":"crossref","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, POPL \u201908, pp.\u00a03\u201315. ACM (2008)","DOI":"10.1145\/1328438.1328443"},{"key":"9287_CR3","unstructured":"Chargu\u00e9raud, A.: http:\/\/www.chargueraud.org\/research\/2006\/poplmark\/ (2006)"},{"issue":"2","key":"9287_CR4","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5(2), 56\u201368 (1940)","journal-title":"J. Symbolic Logic"},{"key":"9287_CR5","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic. North-Holland (1958)"},{"key":"9287_CR6","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"NG Bruijn. de","year":"1972","unstructured":"de\u00a0Bruijn. N.G.: Lambda calculus notation with nameless dummies. A tool for automatic formula manipulation with application to the church-rosser theorem. Indagat. Math. 34, 381\u2013392 (1972)","journal-title":"Indagat. Math."},{"key":"9287_CR7","doi-asserted-by":"crossref","unstructured":"Garrigue, J.: A certified implementation of ML with structural polymorphism. In: Proceedings of the 8th Asian conference on Programming Languages and Systems, APLAS\u201910, pp.\u00a0360\u2013375. Springer-Verlag (2010)","DOI":"10.1007\/978-3-642-17164-2_25"},{"key":"9287_CR8","doi-asserted-by":"crossref","unstructured":"Geuvers, H., Krebbers, R., McKinna, J., Wiedijk, F.: Pure type systems without explicit contexts. In: Proceedings of the 5th International Workshop on Logical Frameworks and Meta-languages (LFMTP), pp.\u00a053\u201367 (2010)","DOI":"10.4204\/EPTCS.34.6"},{"key":"9287_CR9","doi-asserted-by":"crossref","unstructured":"Gordon, A.D.: A mechanisation of name-carrying syntax up to alpha-conversion. In: Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, pp. 413\u2013425. Springer-Verlag (1994)","DOI":"10.1007\/3-540-57826-9_152"},{"key":"9287_CR10","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. J. ACM 40, 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"9287_CR11","unstructured":"Krebbers, R.: A formalization of \u0393\u2009\u221e\u2009 in Coq. http:\/\/robbertkrebbers.nl\/research\/gammainf (2010)"},{"key":"9287_CR12","unstructured":"Leroy, X.: A locally nameless solution to the POPLmark challenge. Research report 6098, INRIA (2007)"},{"key":"9287_CR13","doi-asserted-by":"crossref","unstructured":"Mazurak, K., Zhao, J., Zdancewic, S.: Lightweight linear types in System F\u00b0. In: Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI \u201910, pp.\u00a077\u201388. ACM (2010)","DOI":"10.1145\/1708016.1708027"},{"key":"9287_CR14","doi-asserted-by":"crossref","unstructured":"McKinna, J., Pollack, R.: Pure type systems formalized. In: Proceedings of the International Conference on Typed Lambda Calculi and Applications, pp. 289\u2013305. Springer-Verlag (1993)","DOI":"10.1007\/BFb0037113"},{"key":"9287_CR15","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1023\/A:1006294005493","volume":"23","author":"J McKinna","year":"1999","unstructured":"McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. J. Autom. Reasoning 23, 373\u2013409 (1999)","journal-title":"J. Autom. Reasoning"},{"key":"9287_CR16","unstructured":"Montagu, B.: Experience report: mechanizing core F-zip using the locally nameless approach (extended abstract). In: 5th ACM SIGPLAN Workshop on Mechanizing Metatheory (2010)"},{"key":"9287_CR17","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, PLDI \u201988, pp.\u00a0199\u2013208. ACM (1988)","DOI":"10.1145\/53990.54010"},{"key":"9287_CR18","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pp. 202\u2013206. Springer-Verlag LNAI (1999)","DOI":"10.1007\/3-540-48660-7_14"},{"issue":"2","key":"9287_CR19","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"AM Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"issue":"2","key":"9287_CR20","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10817-011-9229-y","volume":"49","author":"R Pollack","year":"2012","unstructured":"Pollack R., Sato M., Ricciotti, W.: A canonical locally named representation of binding. J. Autom. Reasoning 49(2), 185\u2013207 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"9287_CR21","doi-asserted-by":"crossref","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, TLDI \u201910, pp.\u00a089\u2013102. ACM (2010)","DOI":"10.1145\/1708016.1708028"},{"key":"9287_CR22","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. J. Autom. Reasoning 40, 327\u2013356 (2008)","journal-title":"J. Autom. Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9287-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9287-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9287-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T14:38:11Z","timestamp":1562942291000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9287-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,16]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["9287"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9287-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,16]]}}}