{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T12:06:11Z","timestamp":1699445171949},"reference-count":30,"publisher":"Oxford University Press (OUP)","issue":"2","license":[{"start":{"date-parts":[[2020,1,18]],"date-time":"2020-01-18T00:00:00Z","timestamp":1579305600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,3,16]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>We give an accessible presentation to the foundations of nominal techniques, lying between Zermelo\u2013Fraenkel set theory and Fraenkel\u2013Mostowski set theory, which has several nice properties including being consistent with the Axiom of Choice. We give two presentations of equivariance, accompanied by detailed yet user-friendly discussions of its theory and application.<\/jats:p>","DOI":"10.1093\/logcom\/exz015","type":"journal-article","created":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T19:06:55Z","timestamp":1558897615000},"page":"525-548","source":"Crossref","is-referenced-by-count":3,"title":["Equivariant ZFA and the foundations of nominal techniques"],"prefix":"10.1093","volume":"30","author":[{"given":"Murdoch","family":"Gabbay","sequence":"first","affiliation":[{"name":"Heriot-Watt University, EH144AS Edinburgh, UK"}]}],"member":"286","published-online":{"date-parts":[[2020,1,18]]},"reference":[{"key":"2020041308452625100_ref1","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-10(3:4)2014","article-title":"Automata Theory in Nominal Sets","volume-title":"Logical Methods in Computer Science","author":"Boja\u0144czyk","year":"2014"},{"key":"2020041308452625100_ref2","first-page":"3127","article-title":"Cubical type theory: a constructive interpretation of the univalence axiom","volume":"4","author":"Cohen","year":"2017","journal-title":"IfCoLog Journal of Logics and Their Applications"},{"key":"2020041308452625100_ref3","first-page":"165","volume-title":"Permissive nominal logic (journal version). Transactions on Computational Logic","author":"Dowek","year":"2012"},{"key":"2020041308452625100_ref4","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1016\/j.tcs.2012.06.007","article-title":"PNL to HOL: from the logic of nominal sets to the logic of higher-order functions","volume":"451","author":"Dowek","year":"2012","journal-title":"Theoretical Computer Science"},{"key":"2020041308452625100_ref5","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":"2020041308452625100_ref6","article-title":"Theory of inductive definitions with alpha-equivalence","author":"Gabbay"},{"key":"2020041308452625100_ref7","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1016\/j.jal.2005.10.012","article-title":"Fresh logic","volume":"5","author":"Gabbay","year":"2007","journal-title":"Journal of Applied Logic"},{"key":"2020041308452625100_ref8","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1093\/logcom\/exn055","article-title":"Nominal Algebra and the HSP Theorem","volume":"19","author":"Gabbay","year":"2009","journal-title":"Journal of Logic and Computation"},{"key":"2020041308452625100_ref9","doi-asserted-by":"crossref","first-page":"161","DOI":"10.2178\/bsl\/1305810911","article-title":"Foundations of nominal techniques: logic and semantics of variables in abstract syntax","volume":"17","author":"Gabbay","year":"2011","journal-title":"Bulletin of Symbolic Logic"},{"key":"2020041308452625100_ref10","doi-asserted-by":"crossref","first-page":"828","DOI":"10.2178\/jsl\/1344862164","article-title":"Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free","volume":"77","author":"J. Gabbay","year":"2012","journal-title":"Journal of Symbolic Logic"},{"key":"2020041308452625100_ref11","doi-asserted-by":"crossref","first-page":"967","DOI":"10.1093\/jigpal\/jzs005","article-title":"Meta-variables as infinite lists in nominal terms unification and rewriting","volume":"20","author":"J. Gabbay","year":"2012","journal-title":"Logic Journal of the IGPL"},{"key":"2020041308452625100_ref12","first-page":"178","article-title":"Stone duality for first-order logic: a nominal approach","author":"Gabbay","year":"2014"},{"key":"2020041308452625100_ref13","first-page":"365","volume-title":"Foundations of Software Science and Computation Structures, 14th International Conference (FOSSACS 2011)","author":"Gabbay","year":"2011"},{"key":"2020041308452625100_ref14","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1016\/j.apal.2016.10.001","article-title":"Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness","volume":"168","author":"Gabbay","year":"2017","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020041308452625100_ref15","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":"2020041308452625100_ref16","volume-title":"A New Approach to abstract syntax involving binders. Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS 1999)","author":"Gabbay","year":"1999"},{"key":"2020041308452625100_ref17","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s001650200016","article-title":"A new approach to abstract syntax with variable binding","volume":"13","author":"Gabbay","year":"2001","journal-title":"Formal Aspects of Computing"},{"key":"2020041308452625100_ref18","article-title":"Cylindric Algebras. North Holland, 1971 and 1985","author":"Henkin","journal-title":"Parts I and II."},{"key":"2020041308452625100_ref19","article-title":"Set Theory","author":"Jech","year":"2006"},{"key":"2020041308452625100_ref20","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172066","volume-title":"Notes on Logic and Set Theory","author":"Johnstone","year":"1987"},{"key":"2020041308452625100_ref21","first-page":"475","volume-title":"Proceedings of the 30th Annual IEEE Symposium on Logic in Computer Science (LICS 2015)","author":"Klin","year":"2015"},{"key":"2020041308452625100_ref22","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/978-3-662-47666-6_23","volume-title":"International Colloquium on Automata, Languages, and Programming","author":"Kozen","year":"2015"},{"key":"2020041308452625100_ref23","doi-asserted-by":"crossref","DOI":"10.1016\/j.jlamp.2017.06.002","article-title":"Completeness and incompleteness in Nominal Kleene algebra","volume-title":"Journal of Logical and Algebraic Methods in Programming","author":"Kozen","year":"2017"},{"key":"2020041308452625100_ref24","doi-asserted-by":"crossref","DOI":"10.1145\/2159531.2159532","article-title":"Nominal unification from a higher-order perspective","volume-title":"Transactions on Computational Logic (TOCL)","author":"Levy","year":"2012"},{"key":"2020041308452625100_ref25","first-page":"219","volume-title":"Proc. 4th Int\u2019l Symposium on Theoretical Aspects of Computer Software (TACS 2001) (N. Kobayashi and B. C. Pierce, eds.)","author":"Pitts","year":"2001"},{"key":"2020041308452625100_ref26","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","article-title":"Nominal logic, a first order theory of names and binding","volume":"186","author":"Pitts","year":"2003","journal-title":"Information and Computation"},{"key":"2020041308452625100_ref27","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139084673","volume-title":"Nominal Sets: Names and Symmetry in Computer Science","author":"Pitts","year":"2013"},{"key":"2020041308452625100_ref28","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"The Univalent Foundations Program","year":"2013"},{"key":"2020041308452625100_ref29","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"},{"key":"2020041308452625100_ref30","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","article-title":"Nominal reasoning techniques in Isabelle\/HOL","volume":"40","author":"Urban","year":"2008","journal-title":"Journal of Automatic Reasoning"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/2\/525\/33039963\/exz015.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/2\/525\/33039963\/exz015.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,13]],"date-time":"2020-04-13T12:45:41Z","timestamp":1586781941000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/2\/525\/5670601"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,18]]},"references-count":30,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2020,1,18]]},"published-print":{"date-parts":[[2020,3,16]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exz015","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2020,3]]},"published":{"date-parts":[[2020,1,18]]}}}