{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:15:04Z","timestamp":1774988104450,"version":"3.50.1"},"reference-count":47,"publisher":"Elsevier BV","issue":"12","license":[{"start":{"date-parts":[[2009,12,1]],"date-time":"2009-12-01T00:00:00Z","timestamp":1259625600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,12,1]],"date-time":"2013-12-01T00:00:00Z","timestamp":1385856000000},"content-version":"vor","delay-in-days":1461,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1016\/j.ic.2009.06.004","type":"journal-article","created":{"date-parts":[[2009,8,6]],"date-time":"2009-08-06T09:47:12Z","timestamp":1249552032000},"page":"1369-1400","source":"Crossref","is-referenced-by-count":11,"title":["The lambda-context calculus (extended version)"],"prefix":"10.1016","volume":"207","author":[{"given":"Murdoch J.","family":"Gabbay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Lengrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/j.ic.2009.06.004_bib1","series-title":"Proceedings of the 13th IEEE Symposium on Logic in Computer Science","first-page":"334","article-title":"A fully abstract game semantics for general references","author":"Abramsky","year":"1998"},{"key":"10.1016\/j.ic.2009.06.004_bib2","series-title":"Term Rewriting and All That","author":"Baader","year":"1998"},{"key":"10.1016\/j.ic.2009.06.004_bib3","series-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"10.1016\/j.ic.2009.06.004_bib4","series-title":"Handbook of Mathematical Logic","first-page":"5","article-title":"An introduction to first-order logic","author":"Barwise","year":"1977"},{"key":"10.1016\/j.ic.2009.06.004_bib5","unstructured":"Roel Bloo, Kristoffer H\u00f8gsbro Rose, Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection, in: CSN-95: Computer Science in the Netherlands, 1995."},{"key":"10.1016\/j.ic.2009.06.004_bib6","unstructured":"Mirna Bognar, Contexts in Lambda Calculus, Ph.D. Thesis, Vrije Universiteit Amsterdam, 2002."},{"key":"10.1016\/j.ic.2009.06.004_bib7","series-title":"FOSSACS","first-page":"379","article-title":"A simpler proof theory for nominal logic","author":"Cheney","year":"2005"},{"key":"10.1016\/j.ic.2009.06.004_bib8","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/j.entcs.2007.02.009","article-title":"Nominal equational logic","volume":"172","author":"Clouston","year":"2007","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"2","key":"10.1016\/j.ic.2009.06.004_bib9","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/S0304-3975(97)00150-3","article-title":"A lambda-calculus for dynamic binding","volume":"192","author":"Dami","year":"1998","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"10.1016\/j.ic.2009.06.004_bib10","doi-asserted-by":"crossref","first-page":"917","DOI":"10.1016\/j.ic.2006.12.002","article-title":"Nominal rewriting (journal version)","volume":"205","author":"Fern\u00e1ndez","year":"2007","journal-title":"Information and Computation"},{"key":"10.1016\/j.ic.2009.06.004_bib11","doi-asserted-by":"crossref","unstructured":"Murdoch J. Gabbay, A NEW calculus of contexts, in: PPDP\u201905, ACM, New York, 2005, pp. 94\u2013105.","DOI":"10.1145\/1069774.1069783"},{"issue":"5","key":"10.1016\/j.ic.2009.06.004_bib12","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/j.entcs.2007.01.017","article-title":"Hierarchical nominal terms and their theory of rewriting","volume":"174","author":"Gabbay","year":"2007","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/j.ic.2009.06.004_bib13","volume":"vol. 1","author":"Gabbay","year":"2005"},{"key":"10.1016\/j.ic.2009.06.004_bib14","unstructured":"Murdoch J. Gabbay, Aad Mathijssen, Nominal Algebra, in: Proceedings of the 18th Nordic Workshop on Programming Theory, 2006."},{"issue":"4\u20135","key":"10.1016\/j.ic.2009.06.004_bib15","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s00165-007-0056-1","article-title":"Capture-avoiding substitution as a nominal algebra","volume":"20","author":"Gabbay","year":"2008","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/j.ic.2009.06.004_bib16","unstructured":"Murdoch J. Gabbay, Aad Mathijssen, Nominal algebra, Journal of Logic and Computation (2009) (in press)."},{"key":"10.1016\/j.ic.2009.06.004_bib17","doi-asserted-by":"crossref","unstructured":"Murdoch J. Gabbay, Aad Mathijssen, A nominal axiomatisation of the lambda-calculus, Journal of Logic and Computation (2009) (in press).","DOI":"10.1093\/logcom\/exp049"},{"key":"10.1016\/j.ic.2009.06.004_bib18","unstructured":"Murdoch J. Gabbay, Dominic P. Mulligan, One-and-a-halfth order terms: Curry\u2013Howard for incomplete derivations, in: Proceedings of 15th Workshop on Logic, Language and Information in Computation (WoLLIC 2008), Lecture Notes in Artificial Intelligence, vol. 5110, Springer, Berlin, 2008, pp. 180\u2013194."},{"key":"10.1016\/j.ic.2009.06.004_bib19","doi-asserted-by":"crossref","unstructured":"Murdoch J. Gabbay, Dominic P. Mulligan, One-and-a-halfth order terms: Curry\u2013Howard for incomplete first-order logic derivations using one-and-a-halfth level terms, Information and Computation (2009) (in press).","DOI":"10.1007\/978-3-540-69937-8_16"},{"key":"10.1016\/j.ic.2009.06.004_bib20","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/j.entcs.2009.07.018","article-title":"Two-level lambda-calculus","volume":"246","author":"Gabbay","year":"2009","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"3\u20135","key":"10.1016\/j.ic.2009.06.004_bib21","first-page":"341","article-title":"A new approach to abstract syntax with variable binding","volume":"13","author":"Gabbay","year":"2001","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/j.ic.2009.06.004_bib22","doi-asserted-by":"crossref","unstructured":"Herman Geuvers, Gueorgui I. Jojgov, Open proofs and open terms: a basis for interactive logic, in: CSL, 2002, pp. 537\u2013552.","DOI":"10.1007\/3-540-45793-3_36"},{"key":"10.1016\/j.ic.2009.06.004_bib23","unstructured":"Makoto Hamana, Free sigma-monoids: a higher-order syntax with metavariables, in: The Second Asian Symposium on Programming Languages and Systems (APLAS 2004), Lecture Notes in Computer Science, vol. 3202, Springer, Berlin, 2004, pp. 348\u2013363."},{"issue":"1\u20132","key":"10.1016\/j.ic.2009.06.004_bib24","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/S0304-3975(00)00174-2","article-title":"A typed context calculus","volume":"266","author":"Hashimoto","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.ic.2009.06.004_bib25","doi-asserted-by":"crossref","unstructured":"Dimitri Hendriks, Vincent van Oostrom, Adbmal, in: CADE, 2003, pp. 136\u2013150.","DOI":"10.1007\/978-3-540-45085-6_11"},{"key":"10.1016\/j.ic.2009.06.004_bib26","series-title":"TYPES","first-page":"162","article-title":"Holes with binding power","volume":"vol. 2646","author":"Jojgov","year":"2002"},{"key":"10.1016\/j.ic.2009.06.004_bib27","unstructured":"Samuel Kamin, Jean-Jacques L\u00e9vy, Attempts for generalizing the recursive path orderings, Handwritten paper, University of Illinois, 1980."},{"key":"10.1016\/j.ic.2009.06.004_bib28","series-title":"PLDI","first-page":"24","article-title":"Lazy functional state threads","author":"Launchbury","year":"1994"},{"key":"10.1016\/j.ic.2009.06.004_bib29","series-title":"ICFP\u201996: Proceedings of the First ACM SIGPLAN International Conference on Functional Programming","first-page":"239","article-title":"Enriching the lambda calculus with contexts: toward a theory of incremental program construction","author":"Lee","year":"1996"},{"key":"10.1016\/j.ic.2009.06.004_bib30","series-title":"POPL","first-page":"60","article-title":"From lambda-sigma to lambda-upsilon: a journey through calculi of explicit substitutions","author":"Lescanne","year":"1994"},{"key":"10.1016\/j.ic.2009.06.004_bib31","unstructured":"Aad Mathijssen, Logical calculi for reasoning with binding, Ph.D. Thesis, Technische Universiteit Eindhoven, 2007."},{"issue":"1","key":"10.1016\/j.ic.2009.06.004_bib32","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0890-5401(92)90009-5","article-title":"A calculus of mobile processes, II","volume":"100","author":"Milner","year":"1992","journal-title":"Information and Computation"},{"issue":"1","key":"10.1016\/j.ic.2009.06.004_bib33","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","article-title":"Notions of computation and monads","volume":"93","author":"Moggi","year":"1991","journal-title":"Information and Computation"},{"key":"10.1016\/j.ic.2009.06.004_bib34","unstructured":"Eugenio Moggi, Walid Taha, Zine-El-Abidine Benaissa, Tim Sheard, An idealized metaml: simpler, and more expressive, in: ESOP\u201999 \u2013 Proceedings of the of the Eighth European Symposium on Programming Languages and Systems, Lecture Notes in Computer Science, vol. 1576, Springer, London, 1999, pp. 193\u2013207."},{"key":"10.1016\/j.ic.2009.06.004_bib35","series-title":"Higher Order Operational Techniques in Semantics","first-page":"227","article-title":"Operational reasoning for functions with local state","author":"Pitts","year":"1998"},{"key":"10.1016\/j.ic.2009.06.004_bib36","series-title":"MPC2000","first-page":"230","article-title":"A metalanguage for programming with bound names modulo renaming","volume":"vol. 1837","author":"Pitts","year":"2000"},{"issue":"1\u20132","key":"10.1016\/j.ic.2009.06.004_bib37","first-page":"79","article-title":"Explicit environments","volume":"45","author":"Sato","year":"2001","journal-title":"Fundamenta Informaticae"},{"issue":"4","key":"10.1016\/j.ic.2009.06.004_bib38","first-page":"359","article-title":"A simply typed context calculus with first-class environments","volume":"2002","author":"Sato","year":"2002","journal-title":"Journal of Functional and Logic Programming"},{"key":"10.1016\/j.ic.2009.06.004_bib39","doi-asserted-by":"crossref","unstructured":"Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama, Atsushi Igarashi, Calculi of meta-variables, in: CSL, Lecture Notes in Computer Science, vol. 2803, Springer, Berlin, 2003, pp. 484\u2013497.","DOI":"10.1007\/978-3-540-45220-1_39"},{"key":"10.1016\/j.ic.2009.06.004_bib40","doi-asserted-by":"crossref","unstructured":"Tim Sheard, Simon Peyton Jones, Template meta-programming for Haskell, in: Manuel M.T. Chakravarty (Ed.), ACM SIGPLAN Haskell Workshop 02, ACM, New York, 2002, pp. 1\u201316.","DOI":"10.1145\/581690.581691"},{"key":"10.1016\/j.ic.2009.06.004_bib41","unstructured":"Francois Maurel Sylvain Baro, The qnu and qnuk calculi: name capture and control, Technical report, Universit\u00e9 Paris VII, 2003, Extended Abstract, Pr\u00e9publication PPS\/\/03\/11\/\/n16."},{"issue":"118","key":"10.1016\/j.ic.2009.06.004_bib42","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1006\/inco.1995.1057","article-title":"Parallel reductions in lambda-calculus","volume":"1","author":"Takahashi","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/j.ic.2009.06.004_bib43","unstructured":"Terese. Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 2003."},{"key":"10.1016\/j.ic.2009.06.004_bib44","unstructured":"Laurence Tratt, Compile-time meta-programming in converge, Technical report TR-04-11, Department of Computer Science, King\u2019s College London, 2002."},{"issue":"1\u20133","key":"10.1016\/j.ic.2009.06.004_bib45","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1016\/j.tcs.2004.06.016","article-title":"Nominal unification","volume":"323","author":"Urban","year":"2004","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/j.ic.2009.06.004_bib46","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1093\/jigpal\/5.2.259","article-title":"Modal foundations for predicate logic","volume":"5","author":"van Benthem","year":"1997","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/j.ic.2009.06.004_bib47","first-page":"189","article-title":"Higher-order logic","volume":"vol. 1","author":"van Benthem","year":"2001"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S0890540109001540?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S0890540109001540?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T22:08:32Z","timestamp":1558476512000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540109001540"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,12]]},"references-count":47,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["S0890540109001540"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.ic.2009.06.004","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[2009,12]]}}}