{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:15:38Z","timestamp":1759637738628,"version":"3.41.0"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,1,31]],"date-time":"2018-01-31T00:00:00Z","timestamp":1517356800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,1,31]]},"abstract":"<jats:p>Nominal terms extend first-order terms with nominal features and as such constitute a meta-language for reasoning about the named variables of an object language in the presence of meta-level variables. This article introduces a number of type systems for nominal terms of increasing sophistication and demonstrates their application in the areas of rewriting and equational reasoning. Two simple type systems inspired by Church\u2019s simply typed lambda calculus are presented where only well-typed terms are considered to exist, over which \u03b1-equivalence is then axiomatised. The first requires atoms to be strictly annotated whilst the second explores the consequences of a more relaxed de Bruijn-style approach in the presence of atom-capturing substitution. A final type system of richer ML-like polymorphic types is then given in the style of Curry, in which elements of the term language are deemed typeable or not only subsequent to the definition of alpha-equivalence. Principal types are shown to exist and an inference algorithm given to compute them. This system is then used to define two presentations of typed nominal rewriting, one more expressive and one more efficient, the latter also giving rise to a notion of typed nominal equational reasoning.<\/jats:p>","DOI":"10.1145\/3161558","type":"journal-article","created":{"date-parts":[[2018,2,9]],"date-time":"2018-02-09T13:14:02Z","timestamp":1518182042000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Typed Nominal Rewriting"],"prefix":"10.1145","volume":"19","author":[{"given":"Elliot","family":"Fairweather","sequence":"first","affiliation":[{"name":"King\u2019s College London, Department of Informatics, Aldwych, London"}]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[{"name":"King\u2019s College London, Department of Informatics, Aldwych, London"}]}],"member":"320","published-online":{"date-parts":[[2018,2,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003500"},{"volume-title":"Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD\u201916)","year":"2016","author":"Ayala-Rinc\u00f3n Mauricio","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"volume-title":"Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.).","author":"Baader Franz","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19740201902"},{"key":"e_1_2_1_6_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"103","author":"Barendregt Henk P.","year":"1984"},{"volume-title":"Handbook of Logic in Computer Science","author":"Barendregt Henk P.","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Henk P. Barendregt Will Dekkers and Richard Statman. 2013. Lambda Calculus with Types. Cambridge University Press.   Henk P. Barendregt Will Dekkers and Richard Statman. 2013. Lambda Calculus with Types. Cambridge University Press.","DOI":"10.1017\/CBO9781139032636"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2009.10.003"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_30"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.115"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9164-3"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"James Cheney. 2012. A dependent nominal type theory. Logic. Methods Comput. Sci. 8 1 (2012).  James Cheney. 2012. A dependent nominal type theory. Logic. Methods Comput. Sci. 8 1 (2012).","DOI":"10.2168\/LMCS-8(1:8)2012"},{"volume-title":"Proceedings of the Conference on Uniform Distribution Theory (UNIF\u201903)","year":"2003","author":"Cheney James","key":"e_1_2_1_14_1"},{"volume-title":"Proceedings of the 20th International Conference on Logic Programming (ICLP\u201904)","year":"2004","author":"Cheney James","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387675"},{"key":"e_1_2_1_17_1","unstructured":"Adam Chlipala. 2011. Certified Programming with Dependent Types. MIT Press.   Adam Chlipala. 2011. Certified Programming with Dependent Types. MIT Press."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"e_1_2_1_20_1","unstructured":"Manuel Clavel Francisco Dur\u00e1n Steven Eker Patrick Lincoln Narciso Mart\u00ed-Oliet Jos\u00e9 Meseguer and Carolyn Talcott. 2011. Maude Manual. Retrieved from http:\/\/maude.cs.uiuc.edu\/maude2-manual\/maude-manual.pdf.  Manuel Clavel Francisco Dur\u00e1n Steven Eker Patrick Lincoln Narciso Mart\u00ed-Oliet Jos\u00e9 Meseguer and Carolyn Talcott. 2011. Maude Manual. Retrieved from http:\/\/maude.cs.uiuc.edu\/maude2-manual\/maude-manual.pdf."},{"key":"e_1_2_1_21_1","unstructured":"Ranald A. Clouston. 2007. Closed terms (unpublished notes). Retrieved from http:\/\/users.cecs.anu.edu.au\/rclouston\/closedterms.pdf.  Ranald A. Clouston. 2007. Closed terms (unpublished notes). Retrieved from http:\/\/users.cecs.anu.edu.au\/rclouston\/closedterms.pdf."},{"key":"e_1_2_1_22_1","unstructured":"Ranald A. Clouston. 2010. Equational Logic for Names and Binding. Ph.D. Dissertation. University of Cambridge.  Ranald A. Clouston. 2010. Equational Logic for Names and Binding. Ph.D. Dissertation. University of Cambridge."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.009"},{"key":"e_1_2_1_24_1","unstructured":"Coq Development Team. 2012. The Coq Proof Assistant: Reference Manual. Retrieved from http:\/\/coq.inria.fr\/distrib\/current\/refman\/.  Coq Development Team. 2012. The Coq Proof Assistant: Reference Manual. Retrieved from http:\/\/coq.inria.fr\/distrib\/current\/refman\/."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.009"},{"key":"e_1_2_1_26_1","unstructured":"Haskell B. Curry and Robert Feys. 1958. Combinatory Logic. Vol. 1. North-Holland.  Haskell B. Curry and Robert Feys. 1958. Combinatory Logic. Vol. 1. North-Holland."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_1_29_1","unstructured":"Elliot Fairweather. 2014. Type Systems for Nominal Terms. Ph.D. Dissertation. King\u2019s College London.  Elliot Fairweather. 2014. Type Systems for Nominal Terms. Ph.D. Dissertation. King\u2019s College London."},{"volume-title":"Proceedings of the 18th International Symposium on Fundamentals of Computation Theory (FCT\u201911)","author":"Fairweather Elliot","key":"e_1_2_1_30_1"},{"volume-title":"Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA\u201915)","year":"2015","author":"Fairweather Elliot","key":"e_1_2_1_31_1"},{"volume":"4502","volume-title":"Proceedings of the Conference on Types for Proofs and Programs (TYPES\u201906)","author":"Fern\u00e1ndez Maribel","key":"e_1_2_1_32_1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.12.002"},{"volume-title":"Proceedings of the 5th International Workshop on Logical Frameworks and Meta-Languages (LFMTP\u201910)","author":"Fern\u00e1ndez Maribel","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013963.1013978"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1305810911"},{"volume-title":"Handbook of Philosphical Logic.","author":"Gabbay Murdoch J.","key":"e_1_2_1_38_1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exp033"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exp049"},{"volume-title":"Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS\u201999)","author":"Murdoch","key":"e_1_2_1_41_1"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90107-S"},{"volume-title":"Proceedings of the 2nd IEEE Symposium on Logic in Computer Science (LICS\u201987)","year":"1987","author":"Harper Robert","key":"e_1_2_1_43_1"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(73)90301-X"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_5"},{"volume-title":"Processes, Terms and Cycles: Steps on the Road to Infinity","author":"Jouannaud Jean-Pierre","key":"e_1_2_1_46_1"},{"key":"e_1_2_1_47_1","unstructured":"Jean-Pierre Jouannaud Femke van Raamsdonk and Albert Rubio. 2005. Higher-Order Rewriting with Types and Arities. (2005). Retrieved from http:\/\/www.lix.polytechnique.fr\/jouannaud\/articles\/horta.pdf.  Jean-Pierre Jouannaud Femke van Raamsdonk and Albert Rubio. 2005. Higher-Order Rewriting with Types and Arities. (2005). Retrieved from http:\/\/www.lix.polytechnique.fr\/jouannaud\/articles\/horta.pdf."},{"key":"e_1_2_1_48_1","volume-title":"Mathematical Centre Tracts","volume":"127","author":"Klop Jan-Willem","year":"1980"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00143-6"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(84)90017-1"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1160074.1159811"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_2_1_56_1","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press.   Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press."},{"key":"e_1_2_1_57_1","doi-asserted-by":"crossref","unstructured":"Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. MIT Press.   Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. MIT Press.","DOI":"10.7551\/mitpress\/1104.001.0001"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147954.1147961"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706321"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.04.003"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.039"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.44"},{"volume-title":"Proceedings of International K Workshop (K\u201914)","year":"2014","author":"Rosu Grigore","key":"e_1_2_1_63_1"},{"key":"e_1_2_1_64_1","unstructured":"Bertrand Russell and Alfred North Whitehead. 1910 1912 1913. Principia Mathematica. Cambridge University Press.  Bertrand Russell and Alfred North Whitehead. 1910 1912 1913. Principia Mathematica. Cambridge University Press."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_20"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944729"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.06.016"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2617"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00548-0"},{"key":"e_1_2_1_72_1","unstructured":"Makarius Wenzel. 2013. The Isabelle Reference Manual. Retrieved from http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/Isabelle2013-2\/doc\/isa%r-ref.pdf.  Makarius Wenzel. 2013. The Isabelle Reference Manual. Retrieved from http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/Isabelle2013-2\/doc\/isa%r-ref.pdf."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3161558","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3161558","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:26:53Z","timestamp":1750213613000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3161558"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,31]]},"references-count":70,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1,31]]}},"alternative-id":["10.1145\/3161558"],"URL":"https:\/\/doi.org\/10.1145\/3161558","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2018,1,31]]},"assertion":[{"value":"2016-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-02-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}