gabbay.bib
@article{gabbay:algub,
author = {Gabbay, Murdoch J.},
publisher = {Cambridge University Press},
date = {2022},
doi = {10.1017/S0960129521000438},
journaltitle = {Mathematical Structures in Computer Science},
note = {See also arXiv preprint https://arxiv.org/abs/2007.12404},
pages = {1--56},
title = {Algebras of UTxO blockchains}
}
@incollection{gabbay:karmb,
author = {Basu, Devraj and Gabbay, Murdoch J.},
editor = {Grech, Alex},
publisher = {Emerald Publishing Limited, Bingley},
booktitle = {Media, Technology and Education in a Post-Truth Society},
date = {2021},
doi = {10.1108/978-1-80043-906-120211016},
note = {See also arXiv preprint https://arxiv.org/abs/2007.13346},
pages = {225--241},
title = {Karl Marx and the Blockchain}
}
@inproceedings{gabbay:utxabs,
author = {Brünjes, Lars and Gabbay, Murdoch J.},
publisher = {Springer},
booktitle = {Proceedings of the 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2020)},
date = {2020-10},
note = {See arXiv preprint https://arxiv.org/abs/2003.14271},
title = {{UTxO}- vs account-based smart contract blockchain programming paradigms}
}
@article{gabbay:equzfn,
abstract = {{We give an accessible presentation to the foundations of nominal techniques, lying between Zermelo–Fraenkel set theory and Fraenkel–Mostowski 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.}},
author = {Gabbay, Murdoch J.},
url = {https://doi.org/10.1093/logcom/exz015},
date = {2020-02},
doi = {10.1093/logcom/exz015},
eprint = {https://academic.oup.com/logcom/advance-article-pdf/doi/10.1093/logcom/exz015/31872862/exz015.pdf},
issn = {0955-792X},
issue = {2},
journaltitle = {Journal of Logic and Computation},
pages = {525--548},
title = {{Equivariant ZFA and the foundations of nominal techniques}},
volume = {30}
}
@article{gabbay:lanssc,
author = {Gabbay, Murdoch J.},
url = {https://doi.org/10.23638/LMCS-14(2:12)2018},
date = {2018-05},
doi = {10.23638/LMCS-14(2:12)2018},
journaltitle = {Logical Methods in Computer Science},
note = {See arXiv preprint arxiv.org/abs/1705.07767},
number = {2, Article 12},
title = {The language of Stratified Sets is confluent and strongly normalising},
volume = {14}
}
@article{ayalarincon:cheonr,
author = {Ayala-Rincón, Mauricio and Fernández, Maribel and Gabbay, Murdoch James and Rocha-Oliveira, Ana Cristina},
date = {2016-07},
doi = {http://dx.doi.org/10.1016/j.entcs.2016.06.004},
issn = {1571-0661},
journaltitle = {Electronic Notes in Theoretical Computer Science},
note = {Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015)},
pages = {39--56},
title = {Checking Overlaps of Nominal Rewriting Rules},
volume = {323}
}
@article{gabbay:semooc,
author = {Gabbay, Murdoch J.},
date = {2016-06},
issn = {1535-9921},
journaltitle = {Journal of the ACM},
note = {See also arXiv preprint arxiv.org/abs/1305.6291},
number = {3},
pages = {1--66},
title = {\href{http://www.gabbay.org.uk/papers.html\#semooc}{Semantics out of context: nominal absolute denotations for first-order logic and computation}},
volume = {63}
}
@article{gabbay:repdul,
author = {Gabbay, Murdoch J. and Gabbay, Michael J.},
publisher = {Elsevier},
date = {2017-03},
journaltitle = {Annals of Pure and Applied Logic},
pages = {501--621},
title = {\href{http://www.gabbay.org.uk/papers.html\#repdul-tr}{Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness}},
volume = {168}
}
@inproceedings{gabbay:leatnn,
author = {Gabbay, Murdoch J. and Ghica, Dan R. and Petrisan, Daniela},
editor = {Kreutzer, Stephan},
location = {Dagstuhl, Germany},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
url = {http://drops.dagstuhl.de/opus/volltexte/2015/5426},
annotation = {Keywords: nominal sets, scope, alpha equivalence, dynamic sequences},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
date = {2015},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2015.374},
isbn = {978-3-939897-90-3},
issn = {1868-8969},
pages = {374--389},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {{Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes}},
volume = {41}
}
@article{gabbay:qualps,
author = {Gabbay, Murdoch J. and Wirth, Claus-Peter},
date = {2015},
doi = {10.1093/logcom/exs057},
file = {http://www.gabbay.org.uk/papers/qualps.pdf},
journaltitle = {Journal of Logic and Computation},
number = {2},
pages = {473--523},
title = {\href{http://www.gabbay.org.uk/papers.html\#qualps}{Quantifiers in logic and proof-search using permissive-nominal terms and sets}},
volume = {25}
}
@article{gabbay:simcmt,
author = {Gabbay, Michael J. and Gabbay, Murdoch J.},
date = {2014-11},
issue = {2},
journaltitle = {IFCoLog Journal of Logic and its Applications},
title = {A Simple and Complete Model Theory for Intensional and Extensional Untyped Lambda-Equality},
volume = {1}
}
@article{gabbay:dencmt,
author = {Gabbay, Murdoch J. and Nanevski, Aleksandar},
date = {2013-03},
doi = {10.1016/j.jal.2012.07.002},
file = {http://www.gabbay.org.uk/papers/dencmt.pdf},
issue = {1},
journaltitle = {Journal of Applied Logic},
pages = {1--29},
title = {\href{http://www.gabbay.org.uk/papers.html\#dencmt}{Denotation of contextual modal type theory (CMTT): syntax and metaprogramming}},
volume = {11}
}
@article{gabbay:pnlthf,
author = {Dowek, Gilles and Gabbay, Murdoch J.},
date = {2012},
doi = {10.1016/j.tcs.2012.06.007},
file = {http://www.gabbay.org.uk/papers/pnlthf.pdf},
journaltitle = {Theoretical Computer Science},
pages = {38--69},
title = {\href{http://www.gabbay.org.uk/papers.html\#pnlthf}{PNL to HOL: from the logic of nominal sets to the logic of higher-order functions}},
volume = {451}
}
@inproceedings{gabbay:nomspl,
author = {Dowek, Gilles and Gabbay, Murdoch J.},
booktitle = {Proceedings of the 9th Italian Convention on Computational Logic ({CILC} 2012)},
date = {2012},
doi = {http://nbn-resolving.de/urn:nbn:de:0074-857-8},
file = {http://www.gabbay.org.uk/papers/nomspl.pdf},
series = {{CEUR} workshop proceedings},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomspl}{Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits}},
volume = {857}
}
@article{gabbay:imaglm,
author = {Gabbay, Murdoch J. and Kropholler, Peter},
publisher = {Cambridge University Press},
date = {2013-10},
file = {http://www.gabbay.org.uk/papers/imaglm.pdf},
journaltitle = {Mathematical Structures in Computer Science},
number = {05},
pages = {1002--1031},
title = {\href{http://www.gabbay.org.uk/papers.html\#imaglm}{Imaginary groups: lazy monoids and reversible computation.}},
volume = {23}
}
@inproceedings{gabbay:gamsnm,
author = {Gabbay, Murdoch J. and Ghica, Dan R.},
booktitle = {Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics ({MFPS} 2012)},
date = {2012},
doi = {10.1016/j.entcs.2012.08.012},
file = {http://www.gabbay.org.uk/papers/gamsnm.pdf},
series = {Electronic Notes in Theoretical Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#gamsnm}{Game semantics in the nominal model}}
}
@article{gabbay:finisn,
author = {Gabbay, Murdoch J.},
publisher = {Duke University Press},
date = {2012-09},
doi = {http://projecteuclid.org/euclid.jsl/1344862164},
file = {http://www.gabbay.org.uk/papers/finisn.pdf},
journaltitle = {Journal of Symbolic Logic},
number = {3},
pages = {828--852},
title = {\href{http://www.gabbay.org.uk/papers.html\#finsin}{Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free}},
volume = {77}
}
@article{gabbay:uniner,
author = {Gabbay, Murdoch J.},
date = {2012-06},
doi = {10.1016/j.jal.2012.03.001},
file = {http://www.gabbay.org.uk/papers/uniner.pdf},
journaltitle = {Journal of Applied Logic},
number = {2},
pages = {199--217},
title = {\href{http://www.gabbay.org.uk/papers.html\#uniner}{Unity in nominal equational reasoning: The algebra of equality on nominal sets}},
volume = {10}
}
@article{gabbay:metvil,
author = {Gabbay, Murdoch J.},
publisher = {Oxford University Press},
date = {2012},
file = {http://www.gabbay.org.uk/papers/metvil.pdf},
journaltitle = {Logic Journal of the {IGPL}},
number = {6},
pages = {967--1000},
title = {\href{http://www.gabbay.org.uk/papers.html\#metvil}{Meta-variables as infinite lists in nominal terms unification and rewriting}},
volume = {20}
}
@incollection{gabbay:stodfo,
author = {Gabbay, Murdoch J.},
publisher = {Easychair books},
booktitle = {HOWARD-60. A Festschrift on the Occasion of Howard Barringer's 60th Birthday},
date = {2014},
pages = {178--209},
title = {\href{http://www.gabbay.org.uk/papers.html\#stodfo}{Stone duality for First-Order Logic: a nominal approach}}
}
@inproceedings{gabbay:nomhss,
author = {Gabbay, Murdoch J. and Mulligan, Dominic P.},
booktitle = {Proceedings of the 6th International Workshop on Logical Frameworks and Meta-Languages ({LFMTP} 2011)},
date = {2011-09},
doi = {10.4204/EPTCS.71.5},
file = {http://www.gabbay.org.uk/papers/nomhss.pdf},
pages = {58--75},
series = {EPTCS},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomhss}{Nominal {H}enkin {S}emantics: simply-typed lambda-calculus models in nominal sets}},
volume = {71}
}
@incollection{gabbay:nomtnl,
author = {Gabbay, Murdoch J.},
publisher = {Kluwer},
booktitle = {Handbook of Philosophical Logic},
date = {2013},
file = {http://www.gabbay.org.uk/papers/nomtnl.pdf},
note = {Survey monograph},
pages = {79--178},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomtnl}{Nominal terms and nominal logics: from foundations to meta-mathematics}},
volume = {17}
}
@article{gabbay:twolns,
author = {Gabbay, Murdoch J.},
publisher = {Cambridge University Press},
date = {2011},
doi = {10.1017/S0960129511000272},
file = {http://www.gabbay.org.uk/papers/twolns.pdf},
journaltitle = {Mathematical Structures in Computer Science},
number = {5},
pages = {997--1033},
title = {\href{http://www.gabbay.org.uk/papers.html\#twolns}{Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables}},
volume = {21}
}
@inproceedings{gabbay:stodnb,
author = {Gabbay, Murdoch J. and Litak, Tadeusz and Petrişan, Daniela},
publisher = {Springer},
booktitle = {Proceedings of the 4th international conference on algebra and coalgebra in computer science ({CALCO} 2011)},
date = {2011},
doi = {10.1007/978-3-642-22944-2\_14},
isbn = {978-3-642-22943-5},
pages = {192--207},
series = {Lecture Notes in Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#stodnb}{Stone duality for nominal Boolean algebras with NEW}},
volume = {6859}
}
@inproceedings{gabbay:frenrs,
author = {Gabbay, Murdoch J. and Ciancia, Vincenzo},
publisher = {Springer},
booktitle = {Foundations of software science and computation structures, 14th International Conference ({FOSSACS} 2011)},
date = {2011},
doi = {10.1007/978-3-642-19805-2\_25},
pages = {365--380},
series = {Lecture Notes in Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#frenrs}{Freshness and name-restriction in sets of traces with names}},
volume = {6604}
}
@article{gabbay:pernl-jv,
author = {Dowek, Gilles and Gabbay, Murdoch J.},
location = {New York},
publisher = {ACM},
date = {2012},
doi = {10.1145/2287718.2287720},
file = {http://www.gabbay.org.uk/papers/pernl-jv.pdf},
journaltitle = {Transactions on Computational Logic},
number = {3},
pages = {165--176},
title = {\href{http://www.gabbay.org.uk/papers.html\#pernl-jv}{Permissive Nominal Logic (journal version)}},
volume = {13}
}
@inproceedings{gabbay:pernl,
author = {Dowek, Gilles and Gabbay, Murdoch J.},
location = {New York},
publisher = {ACM Press},
booktitle = {Proceedings of the 12th International {ACM} {SIGPLAN} Symposium on Principles and Practice of Declarative Programming ({PPDP} 2010)},
date = {2010},
doi = {10.1145/1836089.1836111},
file = {http://www.gabbay.org.uk/papers/pernl.pdf},
pages = {165--176},
title = {\href{http://www.gabbay.org.uk/papers.html\#pernl-cv}{Permissive Nominal Logic}}
}
@article{gabbay:fountl,
author = {Gabbay, Murdoch J.},
publisher = {ACM Press},
date = {2011},
doi = {10.2178/bsl/1305810911},
file = {http://www.gabbay.org.uk/papers/fountl.pdf},
journaltitle = {Bulletin of Symbolic Logic},
note = {Survey monograph},
number = {2},
pages = {161--229},
title = {\href{http://www.gabbay.org.uk/papers.html\#fountl}{Foundations of nominal techniques: logic and semantics of variables in abstract syntax}},
volume = {17}
}
@article{gabbay:perntu-jv,
author = {Dowek, Gilles and Gabbay, Murdoch J. and Mulligan, Dominic P.},
date = {2010},
doi = {10.1093/jigpal/jzq006},
file = {http://www.gabbay.org.uk/papers/perntu-jv.pdf},
journaltitle = {Logic Journal of the {IGPL}},
number = {6},
pages = {769--822},
title = {\href{http://www.gabbay.org.uk/papers.html\#perntu-jv}{Permissive Nominal Terms and their Unification: an infinite, co-infinite approach to nominal techniques (journal version)}},
volume = {18}
}
@report{gabbay:perntu-tr,
author = {Dowek, Gilles and Gabbay, Murdoch J. and Mulligan, Dominic P.},
institution = {Heriot-Watt},
date = {2009-02},
number = {HW-MACS-TR-0062},
title = {\href{http://www.gabbay.org.uk/papers.html\#perntu-tr}{Permissive Nominal Terms and their Unification}},
type = {techreport}
}
@inproceedings{gabbay:simcks,
author = {Gabbay, Michael J. and Gabbay, Murdoch J.},
publisher = {Springer},
booktitle = {International Conference on Logic for Programming Artificial Intelligence and Reasoning ({LPAR} 2010)},
date = {2010},
file = {http://www.gabbay.org.uk/papers/simcks.pdf},
pages = {231--254},
series = {Lecture Notes in Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#simcks}{A simple class of {K}ripke-style models in which logic and computation have equal standing}},
volume = {6355}
}
@inproceedings{gabbay:clonre,
author = {Fernández, Maribel and Gabbay, Murdoch J.},
booktitle = {Electronic Proceedings in Theoretical Computer Science},
date = {2010},
doi = {10.4204/EPTCS.34.5},
file = {http://www.gabbay.org.uk/papers/clonre.pdf},
pages = {37--51},
title = {\href{http://www.gabbay.org.uk/papers.html\#clonre}{Closed nominal rewriting and efficiently computable nominal algebra equality}},
volume = {34}
}
@article{gabbay:noma-jv,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
date = {2009-12},
doi = {http://dx.doi.org/10.1093/logcom/exp033},
file = {http://www.gabbay.org.uk/papers/nomuae.pdf},
journaltitle = {Journal of Logic and Computation},
number = {6},
pages = {1455--1508},
title = {Nominal univeral algebra: equational logic with names and binding},
volume = {19}
}
@incollection{gabbay:alogic,
author = {Gabbay, Murdoch J. and Gabbay, Michael J.},
publisher = {College Publications},
booktitle = {We Will Show Them: Essays in Honour of Dov Gabbay},
date = {2005-10},
doi = {http://www.amazon.co.uk/We-Will-Show-Them-Gabbay/dp/1904987125},
file = {http://www.gabbay.org.uk/papers/alogic.pdf},
isbn = {1-904987-25-7},
title = {\href{http://www.gabbay.org.uk/papers.html\#alog}{a-logic}},
volume = {1}
}
@inproceedings{gabbay:alwa,
author = {Gabbay, Murdoch J. and Gabbay, Michael J.},
booktitle = {Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2007)},
date = {2007-06},
file = {http://www.gabbay.org.uk/papers/alwa.pdf},
pages = {47--62},
title = {\href{http://www.gabbay.org.uk/papers.html\#alwa}{a-logic with arrows}}
}
@article{gabbay:alwa-jv,
author = {Gabbay, Murdoch J. and Gabbay, Michael J.},
booktitle = {Postproceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming ({WFLP} 2007)},
date = {2008-07},
doi = {http://dx.doi.org/10.1016/j.entcs.2008.06.031},
file = {http://www.gabbay.org.uk/papers/alwa-jv.pdf},
journaltitle = {Electronic Notes in Theoretical Computer Science},
pages = {3--29},
title = {\href{http://www.gabbay.org.uk/papers.html\#alwa-jv}{a-logic with arrows (journal version)}},
volume = {216}
}
@inproceedings{gabbay:autfms,
author = {Gabbay, Murdoch J.},
booktitle = {Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics ({TPHOLS} 2002)},
date = {2002-08},
file = {http://www.gabbay.org.uk/papers/autfms.pdf},
pages = {60--70},
title = {Automating {F}raenkel-{M}ostowski Syntax}
}
@inproceedings{gabbay:capasn,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
location = {Berlin},
publisher = {Springer},
booktitle = {Proceedings of the 3rd International Colloquium on Theoretical Aspects of Computing ({ICTAC} 2006)},
date = {2006-11},
doi = {10.1007/11921240\_14},
file = {http://www.gabbay.org.uk/papers/capasn.pdf},
pages = {198--212},
series = {Lecture Notes in Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#capasn}{Capture-avoiding Substitution as a Nominal Algebra}},
volume = {4281}
}
@article{gabbay:capasn-jv,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
publisher = {Springer},
date = {2008-06},
doi = {10.1007/11921240\_14},
file = {http://www.gabbay.org.uk/papers/capasn-jv.pdf},
journaltitle = {Formal Aspects of Computing},
number = {4-5},
pages = {451--479},
title = {\href{http://www.gabbay.org.uk/papers.html\#capasn-jv}{Capture-Avoiding Substitution as a Nominal Algebra}},
volume = {20}
}
@inproceedings{gabbay:curhid,
author = {Gabbay, Murdoch J. and Mulligan, Dominic P.},
publisher = {Springer},
booktitle = {Proceedings of 15th Workshop on Logic, Language and Information in Computation ({WoLLIC} 2008)},
date = {2008-06},
doi = {http://dx.doi.org/10.1007/978-3-540-69937-8_16},
file = {http://www.gabbay.org.uk/papers/curhid.pdf},
pages = {180--194},
series = {Lecture Notes in Artificial Intelligence},
title = {\href{http://www.gabbay.org.uk/papers.html\#curhid}{One-and-a-halfth Order Terms: {Curry-Howard} for Incomplete Derivations}},
volume = {5110}
}
@article{gabbay:curhif-jv,
author = {Gabbay, Murdoch J. and Mulligan, Dominic P.},
date = {2010-03},
doi = {http://dx.doi.org/10.1016/j.ic.2009.09.003},
file = {http://www.gabbay.org.uk/papers/curhif.pdf},
journaltitle = {Information and Computation},
number = {3},
pages = {230--258},
title = {\href{http://www.gabbay.org.uk/papers.html\#curhif-jv}{One-and-a-halfth Order Terms: {Curry-Howard} for Incomplete Derivations (journal version)}},
volume = {208}
}
@incollection{gabbay:curstn,
author = {Fernández, Maribel and Gabbay, Murdoch J.},
publisher = {Springer},
booktitle = {Types for Proofs and Programs ({TYPES} 06)},
date = {2007-09},
doi = {10.1007/978-3-540-74464-1\_9},
file = {http://www.gabbay.org.uk/papers/curstn.pdf},
pages = {125--139},
series = {Lecture Notes in Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#curstn}{Curry-style types for nominal terms}},
volume = {4502}
}
@inproceedings{gabbay:fmhotn,
abstract = {FM (Fraenkel-Mostowski) set theory techniques were developed to give good support to inductive reasoning on formal syntax in the presence of $\alpha$-equivalence and variable binding. The original set theory has inspired a Higher-Order Logic (HOL) theory, FM-HOL, presented in this paper. FM-HOL has similar facilities for handling syntax-with-binding to the original set theory, but is mathematically more powerful, introduces several novel features, and is much better suited to machine automation. This paper concentrates on the mathematical aspect of FM-HOL, presenting it as an improved foundation in which to analyse syntax-with-binding.},
author = {Gabbay, Murdoch J.},
editor = {Kamareddine, F.},
booktitle = {35 Years of {A}utomath},
date = {2002-04},
file = {http://www.gabbay.org.uk/papers/fmhotn.pdf},
title = {\href{http://www.gabbay.org.uk/paper.html\#fmhotn}{{FM-HOL}, a higher-order theory of names}}
}
@inproceedings{gabbay-FM-techniques-in-Isabelle,
author = {Gabbay, Murdoch J.},
booktitle = {TPHOLS},
date = {2002-08},
file = {http://www.gabbay.org.uk/papers/fmtii.pdf},
title = {{FM} techniques in {I}sabelle}
}
@article{gabbay:frelog,
author = {Gabbay, Murdoch J.},
publisher = {Elsevier},
date = {2007-06},
doi = {10.1016/j.jal.2005.10.012},
file = {http://www.gabbay.org.uk/papers/frelog.pdf},
journaltitle = {Journal of Applied Logic},
number = {2},
pages = {356--387},
title = {\href{http://www.gabbay.org.uk/papers.html\#frelog}{{F}resh {L}ogic}},
volume = {5}
}
@inproceedings{gabbay:frepbm,
author = {Shinwell, Mark R. and Pitts, Andrew M. and Gabbay, Murdoch J.},
publisher = {ACM Press},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on Functional Programming ({ICFP} 2003)},
date = {2003-08},
doi = {10.1145/944705.944729},
file = {http://www.gabbay.org.uk/papers/frepbm.pdf},
journaltitle = {SIGPLAN Notices},
pages = {263--274},
title = {\href{http://www.gabbay.org.uk/papers.html\#frepbm}{Fresh{ML}: Programming with Binders Made Simple}},
volume = {38}
}
@article{gabbay:genmn,
author = {Gabbay, Murdoch J.},
publisher = {Academic Press},
date = {2007-07},
doi = {http://dx.doi.org/10.1016/j.ic.2006.10.010},
file = {http://www.gabbay.org.uk/papers/genmn.pdf},
journaltitle = {Information and Computation},
number = {7},
pages = {982--1011},
title = {\href{http://www.gabbay.org.uk/papers.html\#genmn}{A General Mathematics of Names}},
volume = {205}
}
@article{gabbay:hienr,
author = {Gabbay, Murdoch J.},
publisher = {Elsevier},
date = {2007-06},
doi = {http://dx.doi.org/10.1016/j.entcs.2007.01.017},
file = {http://www.gabbay.org.uk/papers/hienr.pdf},
issn = {1571-0661},
journaltitle = {Electronic Notes in Theoretical Computer Science},
number = {5},
pages = {37--52},
title = {\href{http://www.gabbay.org.uk/papers.html\#hienr}{Hierarchical Nominal Terms and Their Theory of Rewriting}},
volume = {174}
}
@inproceedings{gabbay:hienr-preproceedings,
author = {Gabbay, Murdoch J.},
booktitle = {Preproceedings of the 1st International Workshop on Logical Frameworks and Meta-Languages ({LFMTP} 2006)},
date = {2006-09},
pages = {32--47},
title = {Hierarchical nominal rewriting}
}
@article{gabbay:lamcc,
author = {Gabbay, Murdoch J. and Lengrand, Stéphane},
publisher = {Elsevier},
date = {2008-01},
doi = {10.1016/j.entcs.2007.09.015},
file = {http://www.gabbay.org.uk/papers/lamcc.pdf},
issn = {1571-0661},
journaltitle = {Electronic Notes in Theoretical Computer Science},
pages = {19--35},
title = {\href{http://www.gabbay.org.uk/papers.html\#lamcc}{The lambda-context calculus}},
volume = {196}
}
@article{gabbay:lamcce,
author = {Gabbay, Murdoch J. and Lengrand, Stéphane},
publisher = {Elsevier},
date = {2009-12},
doi = {10.1016/j.ic.2009.06.004},
issue = {12},
journaltitle = {Information and computation},
pages = {1369--1400},
title = {\href{http://www.gabbay.org.uk/papers.html\#lamcce}{The lambda-context calculus (extended version)}},
volume = {207}
}
@incollection{gabbay:lamcna,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
editor = {Benzmüller, Christoph and Brown, Chad and Siekmann, Jörg and Statman, Rick},
publisher = {IFCoLog},
booktitle = {Reasoning in simple type theory: Festschrift in Honour of {P}eter {B.} {A}ndrews on his 70th Birthday},
date = {2008-12},
file = {http://www.gabbay.org.uk/papers/lamcna.pdf},
series = {Studies in Logic and the Foundations of Mathematics},
title = {\href{http://www.gabbay.org.uk/papers.html\#lamcna}{The lambda-calculus is nominal algebraic}}
}
@inproceedings{gabbay:newcc,
author = {Gabbay, Murdoch J.},
publisher = {ACM Press},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} symposium on Principles and Practice of Declarative Programming ({PPDP} 2005)},
date = {2005-07},
file = {http://www.gabbay.org.uk/papers/newcc.pdf},
pages = {94--105},
title = {\href{http://www.gabbay.org.uk/papers.html\#newcc}{A {NEW} calculus of contexts}}
}
@inproceedings{gabbay:forcie,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
publisher = {Springer},
booktitle = {WoLLIC'07: 14th Workshop on Logic, Language, Information and Computation},
date = {2007-07},
doi = {http://dx.doi.org/10.1007/978-3-540-73445-1_12},
file = {http://www.gabbay.org.uk/papers/forcie.pdf},
pages = {162--176},
series = {Lecture Notes in Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#forcie}{A Formal Calculus for Informal Equality with Binding}},
volume = {4576}
}
@article{gabbay:nomahs,
author = {Gabbay, Murdoch J.},
date = {2009-04},
doi = {10.1093/logcom/exn055},
file = {http://www.gabbay.org.uk/papers/nomahs.pdf},
journaltitle = {Journal of Logic and Computation},
number = {2},
pages = {341--367},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomahs}{Nominal Algebra and the {HSP} Theorem}},
volume = {19}
}
@article{gabbay:nomalc,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
date = {2010-04},
doi = {10.1093/logcom/exp049},
journaltitle = {Journal of Logic and Computation},
number = {2},
pages = {501--531},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomalc}{A nominal axiomatisation of the lambda-calculus}},
volume = {20}
}
@inproceedings{gabbay:noma-nwpt,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
booktitle = {18th Nordic Workshop on Programming Theory},
date = {2006-10},
file = {http://www.gabbay.org.uk/papers/noma-nwpt.pdf},
title = {\href{http://www.gabbay.org.uk/papers.html\#noma-nwpt}{Nominal Algebra}}
}
@report{gabbay:noma-tr,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
institution = {Heriot-Watt},
date = {2006},
number = {HW-MACS-TR-0045},
title = {\href{http://www.gabbay.org.uk/papers.html\#noma-tr}{Nominal Algebra}},
type = {techreport}
}
@inproceedings{gabbay:nomr,
abstract = {In this paper we present a generalization of first-order rewriting which allows us to deal with terms involving binding operations in an elegant and practical way. We use a nominal approach to binding, in which bound entities are explicitly named (rather than using a nameless syntax such as De Bruijn indices), yet we get a rewriting formalism which respects $\alpha$-conversion and has good properties. This is achieved by adapting the powerful techniques for programming with binders developed by Pitts et al. in the FreshML project to the rewriting framework.\par We extend the syntax of first-order terms with simple constructs to represent binding operations. Terms involving binders can be matched against terms naming bound variables explicitly. Nominal rewriting can be seen as higher-order rewriting with first-order syntax.\par We show that standard, first-order, rewriting is a particular case of nominal rewriting, and we also show that very expressive higher-order systems such as Klop's Combinatory Reduction Systems can be easily defined as nominal rewriting systems. Finally we study confluence properties of nominal rewriting.},
author = {Fernández, Maribel and Gabbay, Murdoch J. and Mackie, Ian},
publisher = {ACM Press},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} symposium on Principles and Practice of Declarative Programming ({PPDP} 2004)},
date = {2004-08},
doi = {http://doi.acm.org/10.1145/1013963.1013978},
file = {http://www.gabbay.org.uk/papers/nomr.pdf},
keywords = {variable binding,$\alpha$-conversion,first and higher-order rewriting},
pages = {108--119},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomr}{Nominal Rewriting Systems}}
}
@article{gabbay:nomr-jv,
author = {Fernández, Maribel and Gabbay, Murdoch J.},
date = {2007-06},
doi = {10.1016/j.ic.2006.12.002},
file = {http://www.gabbay.org.uk/papers/nomr-jv.pdf},
journaltitle = {Information and Computation},
number = {6},
pages = {917--965},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomr-jv}{Nominal rewriting (journal version)}},
volume = {205}
}
@inproceedings{gabbay:nomrng,
abstract = {Nominal rewriting extends first-order rewriting with Gabbay-Pitts abstractors: bound entities are explicitly named (rather than being nameless, as for de Bruijn indices) yet rewriting respects $\alpha$-conversion and can be directly implemented, thanks to the use of freshness contexts. In this paper we study two extensions to nominal rewriting. First we introduce a \NEW{} quantifier for modelling name generation. This allows us to model higher-order functions involving local state, and has also applications in concurrency theory. The second extension introduces new constraints in freshness contexts. This allows us to express strategies of reduction and has applications in programming language design and implementation. Finally, we study confluence properties of nominal rewriting and its extensions.},
author = {Fernández, Maribel and Gabbay, Murdoch J.},
publisher = {ACM Press},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Symposium on Principles and Practice of Declarative Programming ({PPDP} 2005)},
date = {2005-07},
doi = {http://doi.acm.org/10.1145/1069774.1069779},
file = {http://www.gabbay.org.uk/papers/nomrng.pdf},
keywords = {Binders,$\alpha$-conversion,first and higher-order rewriting,name generation,locality,confluence},
pages = {47--58},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomrng}{Nominal rewriting with name generation: abstraction vs. locality}}
}
@inproceedings{gabbay:nomrs,
author = {Gabbay, Murdoch J. and Hofmann, Martin},
publisher = {Springer},
booktitle = {Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning ({LPAR} 2008)},
date = {2008-11},
doi = {10.1007/978-3-540-89439-1\_11},
file = {http://www.gabbay.org.uk/papers/nomrs.pdf},
pages = {158--173},
title = {\href{http://www.gabbay.org.uk/papers.html\#rens}{Nominal renaming sets}}
}
@report{gabbay:nomrs-tr,
author = {Gabbay, Murdoch J.},
institution = {Heriot-Watt University},
date = {2007},
file = {http://www.gabbay.org.uk/papers/nomrs-tr.pdf},
number = {HW-MACS-TR-0058},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomrs-tr}{Nominal renaming sets}},
type = {techreport}
}
@inproceedings{gabbay:nomsos-nwpt,
author = {Mousavi, MohammadReza and Gabbay, Murdoch J. and Reniers, Michel A.},
booktitle = {18th Nordic Workshop on Programming Theory},
date = {2006-08},
file = {http://www.gabbay.org.uk/papers/nomsos-nwpt.pdf},
title = {Nominal SOS}
}
@inproceedings{gabbay:nomu,
author = {Urban, Christian and Pitts, Andrew M. and Gabbay, Murdoch J.},
publisher = {Springer},
booktitle = {Proceedings of the 17th International Workshop on Computer Science Logic ({CSL} 2003)},
date = {2003-12},
doi = {10.1016/j.tcs.2004.06.016},
file = {http://www.gabbay.org.uk/papers/nomu.pdf},
pages = {513--527},
series = {Lecture Notes in Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomu}{Nominal Unification}},
volume = {2803}
}
@article{gabbay:nomuae,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
date = {2009-12},
doi = {10.1093/logcom/exp033},
file = {http://www.gabbay.org.uk/papers/nomuae.pdf},
journaltitle = {Journal of Logic and Computation},
number = {6},
pages = {1455--1508},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomuae}{Nominal universal algebra: equational logic with names and binding}},
volume = {19}
}
@article{gabbay:nomu-jv,
author = {Urban, Christian and Pitts, Andrew M. and Gabbay, Murdoch J.},
location = {Essex, UK},
publisher = {Elsevier},
date = {2004-09},
doi = {10.1016/j.tcs.2004.06.016},
file = {http://www.gabbay.org.uk/papers/nomu-jv.pdf},
issn = {0304-3975},
journaltitle = {Theoretical Computer Science},
number = {1--3},
pages = {473--497},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomu-jv}{Nominal Unification}},
volume = {323}
}
@inproceedings{gabbay:oneaah,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
publisher = {ACM},
booktitle = {Proceedings of the 8th {ACM-SIGPLAN} International Symposium on Principles and Practice of Declarative Programming ({PPDP} 2006)},
date = {2006-07},
doi = {10.1145/1140335.1140359},
file = {http://www.gabbay.org.uk/papers/oneaah.pdf},
isbn = {1-59593-388-3},
pages = {189--200},
title = {\href{http://www.gabbay.org.uk/papers.html\#oneaah}{One-and-a-halfth-order logic}}
}
@article{gabbay:oneaah-jv,
author = {Gabbay, Murdoch J. and Mathijssen, Aad},
date = {2008-08},
doi = {10.1093/logcom/exm064},
file = {http://www.gabbay.org.uk/papers/oneaah-jv.pdf},
journaltitle = {Journal of Logic and Computation},
number = {4},
pages = {521--562},
title = {\href{http://www.gabbay.org.uk/papers.html\#oneaah-jv}{One-and-a-halfth-order Logic}},
volume = {18}
}
@inproceedings{gabbay:perntu,
author = {Dowek, Gilles and Gabbay, Murdoch J. and Mulligan, Dominic P.},
booktitle = {Proceedings of the 24th Italian Conference on Computational Logic (CILC'09)},
date = {2009},
file = {http://www.gabbay.org.uk/papers/perntu.pdf},
title = {\href{http://www.gabbay.org.uk/papers.html\#perntu}{Permissive Nominal Terms and their Unification}}
}
@incollection{gabbay:picfm,
author = {Gabbay, Murdoch J.},
editor = {Kamareddine, Fairouz},
publisher = {Kluwer},
booktitle = {Thirty-five years of Automating Mathematics},
date = {2003-11},
doi = {http://www.amazon.co.uk/Thirty-Years-Automating-Mathematics-Applied/dp/1402016565},
file = {http://www.gabbay.org.uk/papers/picfm.pdf},
isbn = {1-4020-1656-5},
pages = {247--269},
series = {Kluwer applied logic series},
title = {\href{http://www.gabbay.org.uk/papers.html\#picfm}{The pi-calculus in {FM}}},
volume = {28}
}
@inproceedings{gabbay:semnt,
author = {Gabbay, Murdoch J. and Mulligan, Dominic P.},
booktitle = {Proceedings of the 2nd International Workshop on the Theory and Applications of Abstraction, Substitution and Naming ({TAASN 2009})},
date = {2009-03},
file = {http://www.gabbay.org.uk/papers/semnt.pdf},
title = {\href{http://www.gabbay.org.uk/papers.html\#semnt}{Semantic nominal terms}}
}
@inproceedings{gabbay:seqcnl,
author = {Gabbay, Murdoch J. and Cheney, James},
publisher = {IEEE Computer Society},
booktitle = {Proceedings of the 19th {IEEE} Symposium on Logic in Computer Science ({LICS} 2004)},
date = {2004-07},
doi = {http://dx.doi.org/10.1109/LICS.2004.6},
file = {http://www.gabbay.org.uk/papers/seqcnl.pdf},
pages = {139--148},
title = {\href{http://www.gabbay.org.uk/papers.html\#seqcnl}{A Sequent Calculus for Nominal Logic}}
}
@incollection{gabbay:somfcg,
author = {Gabbay, Michael J. and Gabbay, Murdoch J.},
editor = {d'Avila Garcez L. C. Lamb J. Woods {S. Artemov}, H. Barringer A. S.},
publisher = {College Publications},
booktitle = {We Will Show Them: Essays in Honour of Dov Gabbay},
date = {2005-10},
doi = {http://www.amazon.co.uk/We-Will-Show-Them-Gabbay/dp/1904987125},
file = {http://www.gabbay.org.uk/papers/somfcg.pdf},
isbn = {1-904987-25-7},
title = {\href{http://www.gabbay.org.uk/papers.html\#somfcg}{Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning}},
volume = {1}
}
@inproceedings{gabbay:soshop,
author = {Mousavi, MohammadReza and Gabbay, Murdoch J. and Reniers, Michel A.},
editor = {Abadi, Martin and de Alfaro, Luca},
publisher = {Springer},
booktitle = {Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05)},
date = {2005-09},
doi = {http://dx.doi.org/10.1007/11539452_25},
file = {http://www.gabbay.org.uk/papers/soshop.pdf},
pages = {308--322},
series = {Lecture Notes in Computer Science},
title = {SOS for Higher Order Processes (Extended Abstract)},
volume = {3653}
}
@article{gabbay:stusun,
author = {Gabbay, Murdoch J.},
publisher = {Elsevier},
date = {2009-03},
doi = {http://dx.doi.org/10.1016/j.tcs.2008.11.013},
file = {http://www.gabbay.org.uk/papers/stusun.pdf},
journaltitle = {Theoretical Computer Science},
number = {12-13},
pages = {1159--1189},
title = {\href{http://www.gabbay.org.uk/papers.html\#stusun}{A study of substitution, using nominal techniques and {F}raenkel-{M}ostowski sets}},
volume = {410}
}
@inproceedings{gabbay:subfmf,
author = {Gabbay, Murdoch J. and Gabbay, Michael},
booktitle = {Proceedings of the 2008 AISB Symposium on Computing and Philosophy},
date = {2008},
file = {http://www.gabbay.org.uk/papers/subfmf-aisb.pdf},
pages = {65--72},
title = {\href{http://www.gabbay.org.uk/papers.html\#subfmf}{Substitution for {F}raenkel-{M}ostowski foundations}}
}
@inproceedings{gabbay:tersl,
author = {Gabbay, Michael and Gabbay, Murdoch J.},
booktitle = {Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008)},
date = {2009-08},
doi = {http://dx.doi.org/10.1016/j.entcs.2009.07.017},
file = {http://www.gabbay.org.uk/papers/tersl.pdf},
pages = {87--106},
series = {Electronic Notes in Theoretical Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#tersl}{Term sequent logic}},
volume = {246}
}
@thesis{gabbay:thesis,
author = {Gabbay, Murdoch J.},
institution = {University of Cambridge, UK},
url = {http://www.gabbay.org.uk/papers.html\#thesis},
date = {2001-03},
file = {http://www.gabbay.org.uk/papers/thesis.pdf},
title = {\href{http://www.gabbay.org.uk/papers.html\#thesis}{A Theory of Inductive Definitions with alpha-Equivalence}},
type = {phdthesis}
}
@inproceedings{gabbay:twollc,
author = {Gabbay, Murdoch J. and Mulligan, Dominic P.},
booktitle = {Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008)},
date = {2009-08},
doi = {http://dx.doi.org/10.1016/j.entcs.2009.07.018},
file = {http://www.gabbay.org.uk/papers/twollc.pdf},
journaltitle = {Electronic Notes in Theoretical Computer Science},
pages = {107--129},
title = {\href{http://www.gabbay.org.uk/papers/twollc.pdf}{Two-level lambda-calculus}},
volume = {246}
}
@inproceedings{gabbay:unialt,
author = {Gabbay, Murdoch J. and Mulligan, Dominic P.},
publisher = {ACM},
booktitle = {Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages ({LFMTP} 2009)},
date = {2009-08},
doi = {http://doi.acm.org/10.1145/1577824.1577835},
file = {http://www.gabbay.org.uk/papers/unialt.pdf},
pages = {64--73},
title = {\href{http://www.gabbay.org.uk/papers/unialt.pdf}{Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables}}
}
@inproceedings{gabbay:newaas,
author = {Gabbay, Murdoch J. and Pitts, Andrew M.},
publisher = {IEEE Computer Society Press},
booktitle = {Proceedings of the 14th Annual Symposium on Logic in Computer Science ({LICS} 1999)},
date = {1999-07},
doi = {10.1109/LICS.1999.782617},
file = {http://www.gabbay.org.uk/papers/newaas.pdf},
pages = {214--224},
title = {\href{http://www.gabbay.org.uk/papers.html\#newaas}{A New Approach to Abstract Syntax Involving Binders}}
}
@article{gabbay:newaas-jv,
author = {Gabbay, Murdoch J. and Pitts, Andrew M.},
date = {2001-07},
doi = {10.1007/s001650200016},
file = {http://www.gabbay.org.uk/papers/newaas-jv.pdf},
journaltitle = {Formal Aspects of Computing},
number = {3--5},
pages = {341--363},
title = {\href{http://www.gabbay.org.uk/papers.html\#newaas-jv}{A New Approach to Abstract Syntax with Variable Binding}},
volume = {13}
}
@inproceedings{gabbay:metpbn,
author = {Pitts, Andrew M. and Gabbay, Murdoch J.},
publisher = {Springer},
booktitle = {Proceedings of the 5th international conference on the mathematics of program construction ({MPC} 2000)},
date = {2000-12},
doi = {http://dx.doi.org/10.1007/10722010_15},
file = {http://www.gabbay.org.uk/papers/metpbn.pdf},
pages = {230--255},
series = {Lecture Notes in Computer Science},
title = {\href{http://www.gabbay.org.uk/papers.html\#metpbn}{A Metalanguage for Programming with Bound Names Modulo Renaming}},
volume = {1837}
}
This file was generated by bibtex2html 1.99.