{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T17:11:05Z","timestamp":1768583465256,"version":"3.49.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","license":[{"start":{"date-parts":[[2008,7,1]],"date-time":"2008-07-01T00:00:00Z","timestamp":1214870400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Substitution is fundamental to the theory of logic and computation. Is substitution something that we define on syntax on a case-by-case basis, or can we turn the idea of substitution into a mathematical object? We give axioms for substitution and prove them sound and complete with respect to a canonical model. As corollaries we obtain a useful conservativity result, and prove that equality-up-to-substitution is a decidable relation on terms. These results involve subtle use of techniques both from rewriting and algebra. A special feature of our method is the use of nominal techniques. These give us access to a stronger assertion language, which includes so-called \u2018freshness\u2019 or \u2018capture-avoidance\u2019 conditions. This means that the sense in which we axiomatise substitution (and prove soundness and completeness) is particularly strong, while remaining quite general.<\/jats:p>","DOI":"10.1007\/s00165-007-0056-1","type":"journal-article","created":{"date-parts":[[2008,1,14]],"date-time":"2008-01-14T08:31:36Z","timestamp":1200299496000},"page":"451-479","source":"Crossref","is-referenced-by-count":29,"title":["Capture-avoiding substitution as a nominal algebra"],"prefix":"10.1145","volume":"20","author":[{"given":"Murdoch J.","family":"Gabbay","sequence":"first","affiliation":[{"name":"School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, Scotland, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aad","family":"Mathijssen","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"The lambda calculus: its syntax and semantics (revised edn)","author":"Barendregt HP","year":"1984"},{"key":"e_1_2_1_2_2_2","unstructured":"Bloo R (1997) Preservation of termination for explicit substitution. PhD Thesis Eindhoven University of Technology Eindhoven"},{"key":"e_1_2_1_2_3_2","unstructured":"Bloo R Rose KH (1995) Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In: CSN-95: computing science in the Netherlands Amsterdam. Stichting Mathematisch Centrum pp 62\u201372"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8130-3"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/12.2.111"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.crma.2004.01.021"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Dowek G Hardin T Kirchner C (2002) Binding logic: proofs and models. In: LPAR\u201902: 9th international conference on logic for programming artificial intelligence and reasoning. Vol 2514 of LNCS. Springer Berlin pp 130\u2013144","DOI":"10.1007\/3-540-36078-6_9"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.2307\/2273585"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.12.002"},{"key":"e_1_2_1_2_11_2","unstructured":"Fiore M Plotkin G Turi D (1999) Abstract syntax and variable binding. In: 14th Annual symposium on logic in computer science Brussels. IEEE Computer Society Press New York pp 193\u2013202"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Fiore M Turi D (2001) Semantics of name and value passing. In: 16th annual symposium on logic in computer science Los Alamitos. IEEE Computer Society Press New York pp 93\u2013104","DOI":"10.1109\/LICS.2001.932486"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.017"},{"key":"e_1_2_1_2_14_2","unstructured":"Gabbay MJ Lengrand S (2007) The lambda-context calculus. In: LFMTP\u201907: international workshop on logical frameworks and meta-languages to be published in ENTCS"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Gabbay MJ Mathijssen A (2006) Capture-avoiding substitution as a nominal algebra. In: Theoretical aspects of computing: ICTAC 2006. Vol 4281 of LNCS. Springer Berlin pp 198\u2013212","DOI":"10.1007\/11921240_14"},{"key":"e_1_2_1_2_16_2","unstructured":"Gabbay MJ Mathijssen A (2006) Nominal algebra. Technical Report HW-MACS-TR-0045 Heriot-Watt"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Gabbay MJ Mathijssen A (2006) One-and-a-halfth-order logic. In: PPDP\u201906: Proc. of the 8th ACM SIGPLAN symposium on principles and practice of declarative programming. ACM Press New York pp 189\u2013200","DOI":"10.1145\/1140335.1140359"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Gabbay MJ Mathijssen A (2007) A formal calculus for informal equality with binding. In: WoLLIC\u201907: 14th workshop on logic language information and computation. Vol 4576 of LNCS. Springer Berlin pp 162\u2013176","DOI":"10.1007\/978-3-540-73445-1_12"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"e_1_2_1_2_20_2","first-page":"1","volume-title":"Handbook of philosophical logic, 2nd edn, Vol 1.","author":"Hodges W","year":"2001"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Huet G (2002) Higher order unification 30\u00a0years later. In: TPHOLs 2002: theorem proving in higher order logics number 2410 in LNCS. Springer Berlin pp 241\u2013258","DOI":"10.1007\/3-540-45685-6_2"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Lescanne P (1994) From \u03bb\u03c3 to \u03bb\u03c5 a journey through calculi of explicit substitutions. In: POPL\u201994: Proceedings of 21st ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM Press New York pp 60\u201369","DOI":"10.1145\/174675.174707"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/7517"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.3.373"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0038698"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00143-6"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00059-1"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00170-9"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Tanaka M Power J (2005) A unified category-theoretic formulation of typed binding signatures. In: MERLIN\u201905: Proceedings of the ACM SIGPLAN workshop on mechanized reasoning about languages with variable binding. ACM Press New York pp 13\u201324","DOI":"10.1145\/1088454.1088457"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.06.016"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0056-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0056-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0056-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:46:04Z","timestamp":1641483964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0056-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7]]},"references-count":31,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["10.1007\/s00165-007-0056-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0056-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,7]]}}}