{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:50:47Z","timestamp":1725742247797},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396335"},{"type":"electronic","value":"9783642396342"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_29","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T13:52:36Z","timestamp":1374501156000},"page":"402-417","source":"Crossref","is-referenced-by-count":11,"title":["Automatically Generated Infrastructure for De Bruijn Syntaxes"],"prefix":"10.1007","author":[{"given":"Emmanuel","family":"Polonowski","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"29_CR1","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"N. Bruijn de","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)\u00a075(5), 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae (Proceedings)"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Necula, G.C., Wadler, P. (eds.) Proceeding of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 3\u201315. ACM (2008)","DOI":"10.1145\/1328438.1328443"},{"key":"29_CR3","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M.J. Gabbay","year":"2001","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing\u00a013, 341\u2013363 (2001)","journal-title":"Formal Aspects of Computing"},{"key":"29_CR4","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. Information and Computation\u00a0186, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"29_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/11532231_4","volume-title":"Automated Deduction \u2013 CADE-20","author":"C. Urban","year":"2005","unstructured":"Urban, C., Tasson, C.: Nominal techniques in isabelle\/hol. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 38\u201353. Springer, Heidelberg (2005)"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. Journal of Automated Reasoning (2011)","DOI":"10.1007\/s10817-011-9225-2"},{"key":"29_CR7","unstructured":"Aydemir, B., Weirich, S.: LNgen: Tool support for locally nameless representations (March 2009)"},{"key":"29_CR8","unstructured":"Polonowski, E.: DBGen User Manual, TR\u2013LACL\u20132012\u20134 This document introduces DBGen, an automatic generator of De Bruijn infrastructure for the Coq proof assistant. TR\u2013LACL\u20132012\u20134 (2012)"},{"key":"29_CR9","unstructured":"Church, A.: The Calculi of Lambda Conversion. Princeton University Press (1941)"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Aydemir","year":"2005","unstructured":"Aydemir, B., et al.: Mechanized metatheory for the masses: The poplmark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"key":"29_CR11","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press (1990)"},{"issue":"1-2","key":"29_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.W. Klop","year":"1993","unstructured":"Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science\u00a0121(1-2), 279\u2013308 (1993)","journal-title":"Theoretical Computer Science"},{"key":"29_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-28869-2_22","volume-title":"Programming Languages and Systems","author":"G. Lee","year":"2012","unstructured":"Lee, G., Oliveira, B.C.D.S., Cho, S., Yi, K.: Gmeta: A generic formal metatheory framework for first-order representations. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol.\u00a07211, pp. 436\u2013455. Springer, Heidelberg (2012)"},{"key":"29_CR14","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1017\/S0956796809990293","volume":"20","author":"P. Sewell","year":"2010","unstructured":"Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strinsa, R.: Ott: Effective tool support for the working semanticist. Journal of Functional Programming\u00a020, 71\u2013122 (2010)","journal-title":"Journal of Functional Programming"},{"key":"29_CR15","unstructured":"Crolard, T., Polonowski, E.: A program logic for higher-order procedural variables and non-local jumps. Technical Report TR-LACL-2011-4, 50 pages (2011-2012)"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Crolard, T., Polonowski, E.: Deriving a Floyd-Hoare logic for non-local jumps from a formul\u00e6-as-types notion of control. Journal of Logic and Algebraic Programming, 181\u2013208 (2012)","DOI":"10.1016\/j.jlap.2012.01.004"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:50:50Z","timestamp":1558317050000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}