@preamble{{\hyphenation{Mathe-ma-ti-sche}}}
@article{gabbay:dencmt,
author = {Murdoch J. Gabbay and Aleksandar Nanevski},
title = {\href{http://www.gabbay.org.uk/papers.html\#dencmt}{Denotation of contextual modal type theory (CMTT): syntax and metaprogramming}},
note = {In press},
journal = {Journal of Applied Logic},
year = {2012},
doi = {10.1016/j.jal.2012.07.002},
pdf = {http://www.gabbay.org.uk/papers/dencmt.pdf}
}
@article{gabbay:pnlthf,
author = {Gilles Dowek and Murdoch J. Gabbay},
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}},
journal = {Theoretical Computer Science},
volume = {451},
pages = {38-69},
year = {2012},
pdf = {http://www.gabbay.org.uk/papers/pnlthf.pdf},
doi = {10.1016/j.tcs.2012.06.007}
}
@inproceedings{gabbay:nomspl,
author = {Gilles Dowek and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomspl}{Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits}},
booktitle = {Proceedings of the 9th Italian Convention on Computational Logic ({CILC} 2012)},
year = {2012},
pdf = {http://www.gabbay.org.uk/papers/nomspl.pdf},
doi = {http://nbn-resolving.de/urn:nbn:de:0074-857-8},
}
@article{gabbay:imaglm,
author = {Murdoch J. Gabbay and Peter Kropholler},
title = {\href{http://www.gabbay.org.uk/papers.html\#imaglm}{Imaginary groups: lazy monoids and reversible computation.}},
journal = {Mathematical Structures in Computer Science},
publisher = {Cambridge University Press},
year = {2012},
note = {In press},
pdf = {http://www.gabbay.org.uk/papers/imaglm.pdf}
}
@inproceedings{gabbay:gamsnm,
author = {Murdoch J. Gabbay and Dan R. Ghica},
title = {\href{http://www.gabbay.org.uk/papers.html\#gamsnm}{Game semantics in the nominal model}},
year = {2012},
series = {Electronic Notes in Theoretical Computer Science},
booktitle = {Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics ({MFPS} 2012)}
}
@article{gabbay:finisn,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#finsin}{Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free}},
journal = {Journal of Symbolic Logic},
month = {September},
volume = {77},
number = {3},
year = {2012},
publisher = {Duke University Press},
doi = {http://projecteuclid.org/euclid.jsl/1344862164},
pdf = {http://www.gabbay.org.uk/papers/finisn.pdf}
}
@article{gabbay:uniner,
journal = {Journal of Applied Logic},
month = {March},
year = {2012},
title = {\href{http://www.gabbay.org.uk/papers.html\#uniner}{Unity in nominal equational reasoning: The algebra of equality on nominal sets}},
author = {Murdoch J. Gabbay},
doi = {10.1016/j.jal.2012.03.001},
pdf = {http://www.gabbay.org.uk/papers/uniner.pdf}
}
@article{gabbay:metvil,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#metvil}{Meta-variables as infinite lists in nominal terms unification and rewriting}},
journal = {Logic Journal of the {IGPL}},
publisher = {Oxford University Press},
year = {2012},
doi = {http://dx.doi.org/10.1093/jigpal/jzs005},
pdf = {http://www.gabbay.org.uk/papers/metvil.pdf}
}
@incollection{gabbay:stodfo,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#stodfo}{Stone duality for First-Order Logic: a nominal approach}},
booktitle = {Howard Barringer Festschrift},
year = {2011},
month = {December}
}
@inproceedings{gabbay:nomhss,
author = {Murdoch J. Gabbay and Dominic Mulligan},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomhss}{Nominal {H}enkin {S}emantics: simply-typed lambda-calculus models in nominal sets}},
month = {September},
series = {EPTCS},
volume = {71},
booktitle = {Proceedings of the 6th International Workshop on Logical Frameworks and Meta-Languages ({LFMTP} 2011)},
pages = {58-75},
year = {2011},
doi = {10.4204/EPTCS.71.5},
pdf = {http://www.gabbay.org.uk/papers/nomhss.pdf}
}
@incollection{gabbay:nomtnl,
author = {Murdoch J. Gabbay},
booktitle = {Handbook of Philosophical Logic},
volume = 17,
title = {\href{http://www.gabbay.org.uk/papers.html\#nomtnl}{Nominal terms and nominal logics: from foundations to meta-mathematics}},
publisher = {Kluwer},
year = 2012,
pdf = {http://www.gabbay.org.uk/papers/nomtnl.pdf}
}
@article{gabbay:twolns,
author = {Murdoch J. Gabbay},
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}},
journal = {Mathematical Structures in Computer Science},
volume = 21,
issue = 5,
pages = {997-1033},
year = {2011},
pdf = {http://www.gabbay.org.uk/papers/twolns.pdf},
doi = {10.1017/S0960129511000272}
}
@inproceedings{gabbay:stodnb,
author = {Murdoch J. Gabbay and Tadeusz Litak and Daniela Petri\c{s}an},
title = {\href{http://www.gabbay.org.uk/papers.html\#stodnb}{Stone duality
for nominal Boolean algebras with NEW}},
booktitle = {Proceedings of the 4th international conference on algebra and coalgebra
in computer science ({CALCO} 2011)},
year = {2011},
volume = {6859},
series = {Lecture Notes in Computer Science},
pages = {192-207},
publisher = {Springer},
doi = {10.1007/978-3-642-22944-2\_14},
isbn = {978-3-642-22943-5}
}
@inproceedings{gabbay:frenrs,
author = {Murdoch J. Gabbay and Vincenzo Ciancia},
title = {\href{http://www.gabbay.org.uk/papers.html\#frenrs}{Freshness and
name-restriction in sets of traces with names}},
booktitle = {Foundations of software science and computation structures, 14th
International Conference ({FOSSACS} 2011)},
year = {2011},
volume = {6604},
series = {Lecture Notes in Computer Science},
pages = {365-380},
publisher = {Springer},
doi = {10.1007/978-3-642-19805-2\_25}
}
@article{gabbay:pernl-jv,
author = {Gilles Dowek and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#pernl-jv}{Permissive Nominal Logic (journal version)}},
volume = {13},
number = {3},
year = {2012},
journal = {Transactions on Computational Logic},
pdf = {http://www.gabbay.org.uk/papers/pernl-jv.pdf}
}
@inproceedings{gabbay:pernl,
author = {Gilles Dowek and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#pernl-cv}{Permissive Nominal Logic}},
booktitle = {Proceedings of the 12th International {ACM} {SIGPLAN} Symposium on Principles and Practice of Declarative Programming ({PPDP} 2010)},
pages = {165-176},
year = {2010},
publisher = {ACM Press},
doi = {10.1145/1836089.1836111},
pdf = {http://www.gabbay.org.uk/papers/pernl.pdf}
}
@article{gabbay:fountl,
author = {Murdoch J. Gabbay},
journal = {Bulletin of Symbolic Logic},
title = {\href{http://www.gabbay.org.uk/papers.html\#fountl}{Foundations of nominal techniques: logic and semantics of variables in abstract syntax}},
volume = 17,
number = 2,
year = 2011,
pages = {161-229},
pdf = {http://www.gabbay.org.uk/papers/fountl.pdf},
doi = {10.2178/bsl/1305810911},
publisher = {ACM Press},
}
@article{gabbay:perntu-jv,
author = {Gilles Dowek and Murdoch J. Gabbay and Dominic P. Mulligan},
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)}},
journal = {Logic Journal of the {IGPL}},
year = {2010},
volume = {18},
number = {6},
pages = {769-822},
pdf = {http://www.gabbay.org.uk/papers/perntu-jv.pdf},
doi = {10.1093/jigpal/jzq006}
}
@techreport{gabbay:perntu-tr,
author = {Gilles Dowek and Murdoch J. Gabbay and Dominic P. Mulligan},
title = {\href{http://www.gabbay.org.uk/papers.html\#perntu-tr}{Permissive Nominal Terms and their Unification}},
institution = {Heriot-Watt},
year = {2009},
month = {February},
number = {HW-MACS-TR-0062}
}
@inproceedings{gabbay:simcks,
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}},
author = {Michael J. Gabbay and Murdoch J. Gabbay},
booktitle = {International Conference on Logic for Programming Artificial Intelligence and Reasoning ({LPAR} 2010)},
year = {2010},
pdf = {http://www.gabbay.org.uk/papers/simcks.pdf}
}
@inproceedings{gabbay:clonre,
author = {Maribel Fern{\'a}ndez and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#clonre}{Closed nominal rewriting and efficiently computable nominal
algebra equality}},
year = {2010},
pages = {37--51},
booktitle = {Electronic Proceedings in Theoretical Computer Science},
volume = 34,
pdf = {http://www.gabbay.org.uk/papers/clonre.pdf},
doi = {10.4204/EPTCS.34.5}
}
@article{gabbay:noma-jv,
author = {Murdoch J. Gabbay and Aad Mathijssen},
journal = {Journal of Logic and Computation},
year = {2009},
volume = {19},
number = {6},
pages = {1455-1508},
month = {December},
title = {Nominal univeral algebra: equational logic with names and binding},
doi = {http://dx.doi.org/10.1093/logcom/exp033},
pdf = {http://www.gabbay.org.uk/papers/nomuae.pdf}
}
@incollection{gabbay:alogic,
author = {Murdoch J. Gabbay and Michael J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#alog}{a-logic}},
booktitle = {We Will Show Them: Essays in Honour of Dov Gabbay},
volume = {1},
publisher = {College Publications},
year = {2005},
month = {October},
isbn = {1-904987-25-7},
pdf = {http://www.gabbay.org.uk/papers/alogic.pdf},
doi = {http://www.amazon.co.uk/We-Will-Show-Them-Gabbay/dp/1904987125}
}
@inproceedings{gabbay:alwa,
author = {Murdoch J. Gabbay and Michael J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#alwa}{a-logic with arrows}},
booktitle = {Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2007)},
month = {June},
year = {2007},
pages = {47--62},
pdf = {http://www.gabbay.org.uk/papers/alwa.pdf}
}
@article{gabbay:alwa-jv,
author = {Murdoch J. Gabbay and Michael J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#alwa-jv}{a-logic with arrows (journal version)}},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {216},
pages = {3--29},
month = {July},
booktitle = {Postproceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming ({WFLP} 2007)},
year = {2008},
pdf = {http://www.gabbay.org.uk/papers/alwa-jv.pdf},
doi = {http://dx.doi.org/10.1016/j.entcs.2008.06.031}
}
@inproceedings{gabbay:autfms,
author = {Murdoch J. Gabbay},
title = {Automating Fraenkel-Mostowski Syntax},
booktitle = {Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics ({TPHOLS} 2002)},
year = {2002},
month = {August},
pages = {60-70},
pdf = {http://www.gabbay.org.uk/papers/autfms.pdf}
}
@inproceedings{gabbay:capasn,
author = {Murdoch J. Gabbay and Aad Mathijssen},
title = {\href{http://www.gabbay.org.uk/papers.html\#capasn}{Capture-avoiding Substitution as a Nominal Algebra}},
booktitle = {{ICTAC} 2006: Theoretical Aspects of Computing},
year = {2006},
month = {November},
pages = {198--212},
series = {Lecture Notes in Computer Science},
volume = {4281},
doi = {10.1007/11921240\_14},
pdf = {http://www.gabbay.org.uk/papers/capasn.pdf}
}
@article{gabbay:capasn-jv,
author = {Murdoch J. Gabbay and Aad Mathijssen},
title = {\href{http://www.gabbay.org.uk/papers.html\#capasn-jv}{Capture-Avoiding Substitution as a Nominal Algebra}},
year = {2008},
doi = {10.1007/11921240\_14},
journal = {Formal Aspects of Computing},
month = {June},
pages = {451--479},
volume = {20},
number = {4-5},
publisher = {Springer},
pdf = {http://www.gabbay.org.uk/papers/capasn-jv.pdf}
}
@inproceedings{gabbay:curhid,
author = {Murdoch J. Gabbay and Dominic P. Mulligan},
title = {\href{http://www.gabbay.org.uk/papers.html\#curhid}{One-and-a-halfth Order Terms: {Curry-Howard} for Incomplete Derivations}},
booktitle = {Proceedings of 15th Workshop on Logic, Language and Information in Computation ({WoLLIC} 2008)},
series = {Lecture Notes in Artificial Intelligence},
volume = {5110},
pages = {180--194},
year = {2008},
month = {June},
publisher = {Springer},
doi = {http://dx.doi.org/10.1007/978-3-540-69937-8_16},
pdf = {http://www.gabbay.org.uk/papers/curhid.pdf}
}
@article{gabbay:curhif-jv,
title = {\href{http://www.gabbay.org.uk/papers.html\#curhif-jv}{One-and-a-halfth Order Terms: {Curry-Howard} for Incomplete Derivations (journal version)}},
author = {Murdoch J. Gabbay and Dominic Mulligan},
journal = {Information and Computation},
volume = {208},
issue = {3},
month = {March},
year = {2010},
pages = {230-258},
doi = {http://dx.doi.org/10.1016/j.ic.2009.09.003},
pdf = {http://www.gabbay.org.uk/papers/curhif.pdf}
}
@incollection{gabbay:curstn,
author = {Maribel Fern{\'a}ndez and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#curstn}{Curry-style types for nominal terms}},
year = {2007},
month = {September},
pages = {125--139},
booktitle = {Types for Proofs and Programs ({TYPES} 06)},
series = {Lecture Notes in Computer Science},
volume = {4502},
publisher = {Springer},
doi = {10.1007/978-3-540-74464-1\_9},
pdf = {http://www.gabbay.org.uk/papers/curstn.pdf}
}
@inproceedings{gabbay:fmhotn,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/paper.html\#fmhotn}{{FM-HOL}, a higher-order theory of names}},
booktitle = {35 Years of {A}utomath},
year = {2002},
editor = {F. Kamareddine},
month = {April},
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.},
pdf = {http://www.gabbay.org.uk/papers/fmhotn.pdf}
}
@inproceedings{gabbay-FM-techniques-in-Isabelle,
author = {Murdoch J. Gabbay},
title = {{FM} techniques in {I}sabelle},
booktitle = {TPHOLS},
year = {2002},
month = {August},
organization = {},
pdf = {http://www.gabbay.org.uk/papers/fmtii.pdf}
}
@article{gabbay:frelog,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#frelog}{{F}resh {L}ogic}},
journal = {Journal of Applied Logic},
doi = {10.1016/j.jal.2005.10.012},
year = {2007},
month = {June},
pages = {356--387},
volume = {5},
number = {2},
publisher = {Elsevier},
pdf = {http://www.gabbay.org.uk/papers/frelog.pdf}
}
@inproceedings{gabbay:frepbm,
author = {Mark R. Shinwell and Andrew M. Pitts and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#frepbm}{Fresh{ML}: Programming with Binders Made Simple}},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on Functional Programming ({ICFP} 2003)},
journal = {SIGPLAN Notices},
volume = {38},
year = {2003},
pages = {263--274},
month = {August},
publisher = {ACM Press},
doi = {10.1145/944705.944729},
pdf = {http://www.gabbay.org.uk/papers/frepbm.pdf}
}
@article{gabbay:genmn,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#genmn}{A General Mathematics of Names}},
month = {July},
year = {2007},
volume = {205},
number = {7},
journal = {Information and Computation},
pages = {982--1011},
publisher = {Academic Press},
doi = {http://dx.doi.org/10.1016/j.ic.2006.10.010},
pdf = {http://www.gabbay.org.uk/papers/genmn.pdf}
}
@article{gabbay:hienr,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#hienr}{Hierarchical Nominal Terms and Their Theory of Rewriting}},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {174},
number = {5},
year = {2007},
month = {June},
issn = {1571-0661},
pages = {37--52},
publisher = {Elsevier},
doi = {http://dx.doi.org/10.1016/j.entcs.2007.01.017},
pdf = {http://www.gabbay.org.uk/papers/hienr.pdf}
}
@inproceedings{gabbay:hienr-preproceedings,
author = {Murdoch J. Gabbay},
title = {Hierarchical nominal rewriting},
month = {September},
year = {2006},
pages = {32--47},
booktitle = {Preproceedings of the 1st International Workshop on Logical Frameworks and Meta-Languages ({LFMTP} 2006)}
}
@article{gabbay:lamcc,
author = {Murdoch J. Gabbay and St{\'e}phane Lengrand},
title = {\href{http://www.gabbay.org.uk/papers.html\#lamcc}{The lambda-context calculus}},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {196},
year = {2008},
month = {January},
issn = {1571-0661},
pages = {19--35},
publisher = {Elsevier},
doi = {10.1016/j.entcs.2007.09.015},
pdf = {http://www.gabbay.org.uk/papers/lamcc.pdf}
}
@article{gabbay:lamcce,
author = {Murdoch J. Gabbay and St{\'e}phane Lengrand},
title = {\href{http://www.gabbay.org.uk/papers.html\#lamcce}{The lambda-context calculus (extended version)}},
journal = {Information and computation},
publisher = {Elsevier},
doi = {10.1016/j.ic.2009.06.004},
year = {2009},
month = {December},
issue = {12},
volume = {207},
pages = {1369-1400}
}
@incollection{gabbay:lamcna,
author = {Murdoch J. Gabbay and Aad Mathijssen},
editor = {Christoph Benzm{\"u}ller and Chad Brown and J{\"o}rg Siekmann and Rick Statman},
booktitle = {Reasoning in simple type theory: Festschrift in Honour of {P}eter {B.} {A}ndrews on his 70th Birthday},
title = {\href{http://www.gabbay.org.uk/papers.html\#lamcna}{The lambda-calculus is nominal algebraic}},
publisher = {IFCoLog},
year = 2008,
month = {December},
series = {Studies in Logic and the Foundations of Mathematics},
pdf = {http://www.gabbay.org.uk/papers/lamcna.pdf}
}
@inproceedings{gabbay:newcc,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#newcc}{A {NEW} calculus of contexts}},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} symposium on Principles and Practice of Declarative Programming ({PPDP} 2005)},
year = {2005},
month = {July},
pages = {94--105},
publisher = {ACM Press},
pdf = {http://www.gabbay.org.uk/papers/newcc.pdf}
}
@inproceedings{gabbay:forcie,
author = {Murdoch J. Gabbay and Aad Mathijssen},
title = {\href{http://www.gabbay.org.uk/papers.html\#forcie}{A Formal Calculus for Informal Equality with Binding}},
booktitle = {WoLLIC'07: 14th Workshop on Logic, Language, Information and Computation},
year = {2007},
month = {July},
pages = {162--176},
series = {Lecture Notes in Computer Science},
volume = {4576},
publisher = {Springer},
pdf = {http://www.gabbay.org.uk/papers/forcie.pdf},
doi = {http://dx.doi.org/10.1007/978-3-540-73445-1_12}
}
@article{gabbay:nomahs,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomahs}{Nominal Algebra and the {HSP} Theorem}},
journal = {Journal of Logic and Computation},
year = {2009},
month = {April},
pages = {341--367},
volume = {19},
number = {2},
doi = {10.1093/logcom/exn055},
pdf = {http://www.gabbay.org.uk/papers/nomahs.pdf}
}
@article{gabbay:nomalc,
author = {Murdoch J. Gabbay and Aad Mathijssen},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomalc}{A nominal axiomatisation of the lambda-calculus}},
year = 2010,
month = {April},
journal = {Journal of Logic and Computation},
volume = {20},
number = 2,
pages = {501-531},
doi = {10.1093/logcom/exp049}
}
@inproceedings{gabbay:noma-nwpt,
author = {Murdoch J. Gabbay and Aad Mathijssen},
title = {\href{http://www.gabbay.org.uk/papers.html\#noma-nwpt}{Nominal Algebra}},
booktitle = {18th Nordic Workshop on Programming Theory},
year = {2006},
month = {October},
pdf = {http://www.gabbay.org.uk/papers/noma-nwpt.pdf}
}
@techreport{gabbay:noma-tr,
author = {Murdoch J. Gabbay and Aad Mathijssen},
title = {\href{http://www.gabbay.org.uk/papers.html\#noma-tr}{Nominal Algebra}},
institution = {Heriot-Watt},
year = {2006},
number = {HW-MACS-TR-0045}
}
@inproceedings{gabbay:nomr,
author = {Maribel Fern{\'a}ndez and Murdoch J. Gabbay and Ian Mackie},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomr}{Nominal Rewriting Systems}},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} symposium on Principles and Practice of Declarative Programming ({PPDP} 2004)},
year = {2004},
month = {August},
doi = {http://doi.acm.org/10.1145/1013963.1013978},
pages = {108--119},
publisher = {ACM Press},
keywords = {variable binding, $\alpha$-conversion, first and higher-order rewriting},
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.},
pdf = {http://www.gabbay.org.uk/papers/nomr.pdf}
}
@article{gabbay:nomr-jv,
author = {Maribel Fern{\'a}ndez and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomr-jv}{Nominal rewriting (journal version)}},
pages = {917--965},
volume = {205},
number = {6},
year = {2007},
month = {June},
journal = {Information and Computation},
doi = {10.1016/j.ic.2006.12.002},
pdf = {http://www.gabbay.org.uk/papers/nomr-jv.pdf}
}
@inproceedings{gabbay:nomrng,
author = {Maribel Fern{\'a}ndez and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomrng}{Nominal rewriting with name generation: abstraction vs. locality}},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Symposium on Principles and Practice of Declarative Programming ({PPDP} 2005)},
year = {2005},
month = {July},
doi = {http://doi.acm.org/10.1145/1069774.1069779},
pages = {47--58},
publisher = {ACM Press},
keywords = {Binders, $\alpha$-conversion, first and higher-order rewriting, name generation, locality, confluence},
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.},
pdf = {http://www.gabbay.org.uk/papers/nomrng.pdf}
}
@inproceedings{gabbay:nomrs,
author = {Gabbay, Murdoch J. and Hofmann, Martin},
title = {\href{http://www.gabbay.org.uk/papers.html\#rens}{Nominal renaming sets}},
booktitle = {Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning ({LPAR} 2008)},
year = {2008},
month = {November},
pages = {158--173},
doi = {10.1007/978-3-540-89439-1\_11},
publisher = {Springer},
pdf = {http://www.gabbay.org.uk/papers/nomrs.pdf}
}
@techreport{gabbay:nomrs-tr,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomrs-tr}{Nominal renaming sets}},
number = {HW-MACS-TR-0058},
institution = {Heriot-Watt University},
year = {2007},
pdf = {http://www.gabbay.org.uk/papers/nomrs-tr.pdf}
}
@inproceedings{gabbay:nomsos-nwpt,
author = {MohammadReza Mousavi and Murdoch J. Gabbay and Michel A. Reniers},
title = {Nominal SOS},
booktitle = {18th Nordic Workshop on Programming Theory},
year = {2006},
month = {August},
pdf = {http://www.gabbay.org.uk/papers/nomsos-nwpt.pdf}
}
@inproceedings{gabbay:nomu,
author = {Christian Urban and Andrew M. Pitts and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomu}{Nominal Unification}},
booktitle = {CSL},
pages = {513--527},
month = {December},
year = 2003,
volume = 2803,
series = {Lecture Notes in Computer Science},
doi = {10.1016/j.tcs.2004.06.016},
publisher = {Springer},
pdf = {http://www.gabbay.org.uk/papers/nomu.pdf}
}
@article{gabbay:nomuae,
title = {\href{http://www.gabbay.org.uk/papers.html\#nomuae}{Nominal universal algebra: equational logic with names and binding}},
author = {Murdoch J. Gabbay and Aad Mathijssen},
journal = {Journal of Logic and Computation},
volume = {19},
number = {6},
month = {December},
year = {2009},
pages = {1455-1508},
doi = {10.1093/logcom/exp033},
pdf = {http://www.gabbay.org.uk/papers/nomuae.pdf}
}
@article{gabbay:nomu-jv,
author = {Christian Urban and Andrew M. Pitts and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#nomu-jv}{Nominal Unification}},
journal = {Theoretical Computer Science},
year = {2004},
volume = {323},
number = {1--3},
issn = {0304-3975},
month = {September},
pages = {473--497},
publisher = {Elsevier},
address = {Essex, UK},
doi = {10.1016/j.tcs.2004.06.016},
pdf = {http://www.gabbay.org.uk/papers/nomu-jv.pdf}
}
@inproceedings{gabbay:oneaah,
author = {Murdoch J. Gabbay and Aad Mathijssen},
title = {\href{http://www.gabbay.org.uk/papers.html\#oneaah}{One-and-a-halfth-order logic}},
booktitle = {Proceedings of the 8th {ACM-SIGPLAN} International Symposium on Principles and Practice of Declarative Programming ({PPDP} 2006)},
year = {2006},
month = {July},
pages = {189--200},
publisher = {ACM},
isbn = {1-59593-388-3},
doi = {10.1145/1140335.1140359},
pdf = {http://www.gabbay.org.uk/papers/oneaah.pdf}
}
@article{gabbay:oneaah-jv,
author = {Murdoch J. Gabbay and Aad Mathijssen},
title = {\href{http://www.gabbay.org.uk/papers.html\#oneaah-jv}{One-and-a-halfth-order Logic}},
journal = {Journal of Logic and Computation},
month = {August},
year = {2008},
volume = {18},
number = {4},
pages = {521--562},
pdf = {http://www.gabbay.org.uk/papers/oneaah-jv.pdf},
doi = {10.1093/logcom/exm064}
}
@inproceedings{gabbay:perntu,
title = {\href{http://www.gabbay.org.uk/papers.html\#perntu}{Permissive Nominal Terms and their Unification}},
author = {Gilles Dowek and Murdoch J. Gabbay and Dominic P. Mulligan},
booktitle = {Proceedings of the 24th Italian Conference on Computational Logic (CILC'09)},
year = {2009},
pdf = {http://www.gabbay.org.uk/papers/perntu.pdf}
}
@incollection{gabbay:picfm,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#picfm}{The pi-calculus in {FM}}},
booktitle = {Thirty-five years of Automating Mathematics},
volume = {28},
month = {November},
pages = {247--269},
publisher = {Kluwer},
series = {Kluwer applied logic series},
year = {2003},
editor = {Fairouz Kamareddine},
isbn = {1-4020-1656-5},
pdf = {http://www.gabbay.org.uk/papers/picfm.pdf},
doi = {http://www.amazon.co.uk/Thirty-Years-Automating-Mathematics-Applied/dp/1402016565}
}
@incollection{gabbay:picfm-preproceedings,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#picfm}{The pi-calculus in {FM}}},
booktitle = {Thirty-five years of {A}utomath},
volume = {28},
publisher = {Kluwer},
series = {Kluwer applied logic series},
year = {2003},
editor = {Fairouz Kamareddine},
pdf = {http://www.gabbay.org.uk/papers/picfm-pp.pdf}
}
@inproceedings{gabbay:semnt,
title = {\href{http://www.gabbay.org.uk/papers.html\#semnt}{Semantic nominal terms}},
author = {Murdoch J. Gabbay and Dominic P. Mulligan},
year = {2009},
month = {March},
booktitle = {Proceedings of the 2nd International Workshop on the Theory and Applications of Abstraction, Substitution and Naming ({TAASN 2009})},
pdf = {http://www.gabbay.org.uk/papers/semnt.pdf}
}
@inproceedings{gabbay:seqcnl,
author = {Murdoch J. Gabbay and James Cheney},
title = {\href{http://www.gabbay.org.uk/papers.html\#seqcnl}{A Sequent Calculus for Nominal Logic}},
booktitle = {Proceedings of the 19th {IEEE} Symposium on Logic in Computer Science ({LICS} 2004)},
pages = {139--148},
year = {2004},
month = {July},
publisher = {IEEE Computer Society},
pdf = {http://www.gabbay.org.uk/papers/seqcnl.pdf},
doi = {http://dx.doi.org/10.1109/LICS.2004.6}
}
@incollection{gabbay:somfcg,
author = {Michael J. Gabbay and Murdoch J. Gabbay},
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}},
booktitle = {We Will Show Them: Essays in Honour of Dov Gabbay},
volume = {1},
editor = {H. Barringer A. S. d'Avila Garcez L. C. Lamb J. Woods {S. Artemov}},
publisher = {College Publications},
year = {2005},
month = {October},
isbn = {1-904987-25-7},
pdf = {http://www.gabbay.org.uk/papers/somfcg.pdf},
doi = {http://www.amazon.co.uk/We-Will-Show-Them-Gabbay/dp/1904987125}
}
@inproceedings{gabbay:soshop,
author = {MohammadReza Mousavi and Murdoch J. Gabbay and Michel A. Reniers},
title = {SOS for Higher Order Processes (Extended Abstract)},
booktitle = {Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05)},
series = {Lecture Notes in Computer Science},
volume = {3653},
pages = {308--322},
editor = {Martin Abadi and Luca de Alfaro},
publisher = {Springer},
year = {2005},
month = {September},
doi = {http://dx.doi.org/10.1007/11539452_25},
pdf = {http://www.gabbay.org.uk/papers/soshop.pdf}
}
@article{gabbay:stusun,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#stusun}{A study of substitution, using nominal techniques and {F}raenkel-{M}ostowski sets}},
journal = {Theoretical Computer Science},
volume = {410},
number = {12-13},
year = {2009},
month = {March},
pages = {1159--1189},
publisher = {Elsevier},
doi = {http://dx.doi.org/10.1016/j.tcs.2008.11.013},
pdf = {http://www.gabbay.org.uk/papers/stusun.pdf}
}
@inproceedings{gabbay:subfmf,
author = {Murdoch J. Gabbay and Michael Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#subfmf}{Substitution for {F}raenkel-{M}ostowski foundations}},
booktitle = {Proceedings of the 2008 AISB Symposium on Computing and Philosophy},
year = {2008},
pages = {65--72},
pdf = {http://www.gabbay.org.uk/papers/subfmf-aisb.pdf}
}
@inproceedings{gabbay:tersl,
title = {\href{http://www.gabbay.org.uk/papers.html\#tersl}{Term sequent logic}},
author = {Michael Gabbay and Murdoch J. Gabbay},
series = {Electronic Notes in Theoretical Computer Science},
volume = {246},
month = {August},
year = {2009},
pages = {87-106},
booktitle = {Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008)},
doi = {http://dx.doi.org/10.1016/j.entcs.2009.07.017},
pdf = {http://www.gabbay.org.uk/papers/tersl.pdf}
}
@phdthesis{gabbay:thesis,
author = {Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#thesis}{A Theory of Inductive Definitions with alpha-Equivalence}},
url = {http://www.gabbay.org.uk/papers.html\#thesis},
school = {University of Cambridge, UK},
year = {2001},
month = {March},
pdf = {http://www.gabbay.org.uk/papers/thesis.pdf}
}
@inproceedings{gabbay:twollc,
title = {\href{http://www.gabbay.org.uk/papers/twollc.pdf}{Two-level lambda-calculus}},
author = {Murdoch J. Gabbay and Dominic P. Mulligan},
volume = {246},
pages = {107--129},
booktitle = {Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008)},
year = {2009},
month = {August},
journal = {Electronic Notes in Theoretical Computer Science},
doi = {http://dx.doi.org/10.1016/j.entcs.2009.07.018},
pdf = {http://www.gabbay.org.uk/papers/twollc.pdf}
}
@inproceedings{gabbay:unialt,
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}},
author = {Murdoch J. Gabbay and Dominic P. Mulligan},
year = {2009},
month = {August},
booktitle = {Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages ({LFMTP} 2009)},
pages = {64--73},
doi = {http://doi.acm.org/10.1145/1577824.1577835},
publisher = {ACM},
pdf = {http://www.gabbay.org.uk/papers/unialt.pdf}
}
@inproceedings{gabbay:newaas,
author = {Murdoch J. Gabbay and Andrew M. Pitts},
title = {\href{http://www.gabbay.org.uk/papers.html\#newaas}{A New Approach to Abstract Syntax Involving Binders}},
booktitle = {Proceedings of the 14th Annual Symposium on Logic in Computer Science ({LICS} 1999)},
year = 1999,
month = {July},
publisher = {IEEE Computer Society Press},
pages = {214--224},
doi = {10.1109/LICS.1999.782617},
pdf = {http://www.gabbay.org.uk/papers/newaas.pdf}
}
@article{gabbay:newaas-jv,
author = {Murdoch J. Gabbay and Andrew M. Pitts},
title = {\href{http://www.gabbay.org.uk/papers.html\#newaas-jv}{A New Approach to Abstract Syntax with Variable Binding}},
journal = {Formal Aspects of Computing},
year = {2001},
month = {July},
volume = {13},
number = {3--5},
pages = {341--363},
doi = {10.1007/s001650200016},
pdf = {http://www.gabbay.org.uk/papers/newaas-jv.pdf}
}
@inproceedings{gabbay:metpbn,
author = {Andrew M. Pitts and Murdoch J. Gabbay},
title = {\href{http://www.gabbay.org.uk/papers.html\#metpbn}{A Metalanguage for Programming with Bound Names Modulo Renaming}},
booktitle = {Proceedings of the 5th international conference on the mathematics of program construction ({MPC} 2000)},
pages = {230--255},
year = 2000,
month = {December},
volume = 1837,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
pdf = {http://www.gabbay.org.uk/papers/metpbn.pdf},
doi = {http://dx.doi.org/10.1007/10722010_15}
}
This file was generated by bibtex2html 1.95.