{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T15:14:57Z","timestamp":1648566897567},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2015,5,15]],"date-time":"2015-05-15T00:00:00Z","timestamp":1431648000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2017,2]]},"abstract":"<jats:p>We extend the simply-typed lambda-calculus with a mechanism for dynamic and incremental rebinding of code. Fragments of open code which can be dynamically <jats:italic>rebound<\/jats:italic> are values. Differently from standard static binding, which is done on a <jats:italic>positional<\/jats:italic> basis, rebinding is done on a <jats:italic>nominal<\/jats:italic> basis, that is, free variables in open code are associated with <jats:italic>names<\/jats:italic> which do not obey \u03b1-equivalence. Moreover, rebinding is <jats:italic>incremental<\/jats:italic>, that is, just a subset of names can be rebound, making possible code specialization, and rebinding can even introduce new names. Finally, rebindings, which are associations between names and terms, are first-class values, and can be manipulated by operators such as overriding and renaming. We define a type system in which the type for a rebinding, in addition to specify an association between names and types (similarly to record types), is also annotated. The annotation says whether or not the domain of the rebinding having this type may contain more names than the ones that are specified in the type. We show soundness of the type system.<\/jats:p>","DOI":"10.1017\/s0960129515000109","type":"journal-article","created":{"date-parts":[[2015,5,15]],"date-time":"2015-05-15T06:50:29Z","timestamp":1431672629000},"page":"94-122","source":"Crossref","is-referenced-by-count":1,"title":["Type safe incremental rebinding"],"prefix":"10.1017","volume":"27","author":[{"given":"DAVIDE","family":"ANCONA","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"PAOLA","family":"GIANNINI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ELENA","family":"ZUCCA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2015,5,15]]},"reference":[{"key":"S0960129515000109_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30175-2_11"},{"key":"S0960129515000109_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680500568X"},{"key":"S0960129515000109_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00150-3"},{"key":"S0960129515000109_ref1","unstructured":"Ancona D. , Giannini P. and Zucca E. (2013). Reconciling positional and nominal binding. In: Graham-Lengrand S. and Paolini L. (eds.) ITRS'12 - Intersection types and Related Systems. Available at: http:\/\/bart.disi.unige.it\/bibliography\/papers\/report\/orders:year\/author:4."},{"key":"S0960129515000109_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.02.004"},{"key":"S0960129515000109_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004257"},{"key":"S0960129515000109_ref7","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2011008"},{"key":"S0960129515000109_ref8","unstructured":"Felleisen M. and Friedman D. P. (1986). Control operators, the SECD-machine, and the lambda-calculus. In: 3rd Working Conference on the Formal Description of Programming Concepts, Ebberup, Denmark 193\u2013219."},{"key":"S0960129515000109_ref12","doi-asserted-by":"crossref","unstructured":"Nanevski A. (2003). From dynamic binding to state via modal possibility. In: PPDP'03, ACM 207\u2013218.","DOI":"10.1145\/888251.888271"},{"key":"S0960129515000109_ref9","unstructured":"Gl\u00fcck R. and J\u00f8rgensen J. (1995). Efficient multi-level generating extensions for program specialization. In: PLILP 259\u2013278."},{"key":"S0960129515000109_ref6","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.45.4"},{"key":"S0960129515000109_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944715"},{"key":"S0960129515000109_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1640134.1640137"},{"key":"S0960129515000109_ref11","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010087314987"},{"key":"S0960129515000109_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"S0960129515000109_ref14","volume-title":"Theoretical Aspects of Object-Oriented Programming","author":"R\u00e9my","year":"1993"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129515000109","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,18]],"date-time":"2019-04-18T04:05:25Z","timestamp":1555560325000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129515000109\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,15]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,2]]}},"alternative-id":["S0960129515000109"],"URL":"https:\/\/doi.org\/10.1017\/s0960129515000109","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,15]]}}}