Scroll down for pdf, djvu (what's that?), and BibTeX of my papers. Click above for a flash-based graphical presentation of my papers. You can download the open source software used to create this map here.
Murdoch J. Gabbay on DBLP (not always up-to-date).

top, Journals, chapters, conferences, tech reports, abstracts, unpublished, thesis.

Foundations of nominal techniques: logic and semantics of variables in abstract syntax Murdoch J. Gabbay, Bulletin of Symbolic Logic, in press.: A survey and update paper describing a view of the logical and semantic foundations of nominal techniques applied to nominal abstract syntax.

fountl [pdf] [djvu]
Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques Gilles Dowek, Murdoch J. Gabbay, and Dominic Mulligan, Logic Journal of the IGPL, 2010.: Permissive nominal terms resemble nominal terms, but using infinite and co-infinite sets of atoms gives a stronger theory of alpha-equivalence with ‘always fresh’ and ‘always alpha-rename’ properties familiar from first-and higher- order syntax. The notion of unifier is based on substitution alone, rather than on nominal terms' notion of substitution plus freshness conditions. We give translations between permissive nominal terms, nominal terms, and higher-order terms. This journal paper extends the conference version and technical report and includes some elements from another conference paper.

perntu-jv [pdf] [djvu] [bib] [DOI]
Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms Murdoch J. Gabbay and Dominic Mulligan, Information and Computation, Volume 208, Issue 3, March 2010, Pages 230-258.: We apply nominal terms to propositions-as-types/proofs-as-terms in the presence of incomplete derivations. Atoms correspond with assumptions, unknowns correspond with incomplete parts of the derivation, and a freshness condition corresponds with the condition that an assumption will be discharged in an unknown part of the derivation. This journal paper expands on the conference version.

curhif-jv [pdf] [djvu] [bib] [DOI]
The lambda-context calculus (extended version) Murdoch J. Gabbay and Stéphane Lengrand, Information and Computation, Volume 207, Issue 12, December 2009, Pages 1369-1400.: An extended version of our LFMTP'07 paper. We present a lambda-calculus whose syntax is populated by variables that behave like meta-variables. It can express both capture-avoiding and capturing substitution (instantiation), and a lot more. This calculus is a testbed for ideas to do with having variables of multiple levels in syntax, as in nominal terms.

lamcce [pdf] [djvu] [bib] [DOI]
A nominal axiomatisation of the lambda-calculus Murdoch J. Gabbay and Aad Mathijssen, Journal of Logic and Computation, Volume 20, Number 2, pages 501-531, April 2010.: We axiomatise the lambda-calculus — alpha-beta-(eta) equivalence — in Nominal Algebra and prove our axioms sound and complete. This is intended to substantiate a claim to nominal terms in general, and Nominal Algebra in particular, as a good syntax in which to express specifications of axiom involving names and binding.

nomalc [pdf] [djvu] [bib] [DOI]
Nominal universal algebra: equational logic with names and binding Murdoch J. Gabbay and Aad Mathijssen, Journal of Logic and Computation, Volume 19, Number 6, December 2009, pages 1455-1508.: We describe Nominal Algebra, a universal algebra based on nominal terms, with primitive support for names and binding. This paper subsumes the conference versions in WOLLIC'07 and NWPT'06, and a 2006 technical report.

nomuae [pdf] [djvu] [bib] [DOI]
A study of substitution, using nominal techniques and Fraenkel-Mostowski sets Murdoch J. Gabbay, Theoretical Computer Science, Volume 410, Issues 12-13, 17 March 2009, Pages 1159-1189.: We show how capture-avoiding substitution can be concretely defined on models of Fraenkel-Mostowski set theory. That is, we have substitution on all mathematical objects, and not only on syntax trees. We do not assume an a priori substitution action; we reduce substitution to more primitive constructions assuming only sets structure. This subsumes the AISB'08 paper, and includes full proofs.

stusun [pdf] [djvu] [bib] [DOI]
Nominal Algebra and the HSP theorem Murdoch J. Gabbay, Journal of Logic and Computation, Volume 19, Number 2, April 2009, pages 341-367.: Nominal Algebra extends universal algebra to nominal terms. The HSP theorem for Nominal Algebra places a limit on the structure of models: any model of a Nominal Algebra theory is part of a quotient of a product of atoms-abstractions of free models. The proofs rather beautiful, if you like nominal sets.

nomahs [pdf] [djvu] [bib] [DOI]
a-logic with arrows (journal version), Murdoch J. Gabbay and Michael J. Gabbay, Electronic Notes in Theoretical Computer Science, Volume 216, 4 July 2008, Pages 3-29.: a-logic has a predicate ‘atom’ which is true of a term when it is a variable symbol. We prove cut-elimination, give a notion of model, prove soundess and completeness, and axiomatise substitution and the lambda-calculus, using ‘atom’ to identify variables. This is a journal version of our WFLP'07 paper, with an improved proof-system.

alwa-jv [pdf] [djvu] [bib] [DOI]
Capture-avoiding Substitution as a Nominal Algebra Murdoch J. Gabbay and Aad Mathijssen, Formal Aspects of Computing, Volume 20, Numbers 4-5, July, 2008, Pages 451-479.: Capture-avoiding substitution is a common feature of specifications of logic and computation, appearing for example in specifications of first-order logic and the lambda-calculus. We axiomatise capture-avoiding substitution using Nominal Algebra. This is a journal version of our ICTAC'06 paper.

capasn-jv [pdf] [djvu] [bib] [DOI]
One-and-a-halfth-order logic Murdoch J. Gabbay and Aad Mathijssen, Journal of Logic and Computation, 2008, Volume 18, Pages 521-562.: We add ‘unknown predicates’ to first-order logic. Thus we add some of the power of higher-order logic to reason schematically over predicates, but we preserve the first-order flavour. We give algebraic and sequent characterisations of derivability, and show correctness with respect to first-order logic. This subsumes the PPDP'06 conference paper.

oneaah-jv [pdf] [djvu] [bib] [DOI]
Nominal Rewriting Maribel Fernandez and Murdoch J. Gabbay, Information and Computation, Volume 205, Issue 6, June 2007, Pages 917-965.: Nominal rewriting is rewriting on nominal terms. This is the journal version of our PPDP'04 paper.

nomr-jv [pdf] [djvu] [bib] [DOI]
Hierarchical nominal terms and their theory of rewriting Murdoch J. Gabbay, Electronic Notes in Theoretical Computer Science, Volume 174, Issue 5, 2 June 2007, Pages 37-52.: We build a theory of rewriting on nominal terms with an infinite hierarchy of ‘meta-level variables’. We use it to examine some case studies, including capture- and non-capture avoiding substitution and the NEW calculus of contexts as rewrite systems. This is a revised and expanded version of a workshop paper which appeared in the proceedings of LFMTP'06.

hienr [pdf] [djvu] [bib] [DOI]
A General Mathematics of Names Murdoch J. Gabbay, Information and Computation, Volume 205, Issue 7, July 2007, Pages 982-1011.: We study a generalisation of Fraenkel-Mostowski set theory which can interpret ‘small = infinite’ as one might like to do for example to model infinitary syntax or infinite behaviour that generates names. This is a problem for vanilla Fraenkel-Mostowski set theory, because of its finite support property.

genmn [pdf] [djvu] [bib] [DOI]
Fresh Logic Murdoch J. Gabbay, Journal of Applied Logic, Volume 5, Issue 2, June 2007, Pages 356-387.: This paper gave the first proof-theory for the NEW quantifier investigated in my thesis.

frelog [pdf] [djvu] [bib] [DOI]
Nominal Unification Christian Urban, Andrew M.Pitts and Murdoch J.Gabbay, Theoretical Computer Science, Volume 323, Issues 1-3, 14 September 2004, Pages 473-497.: This paper introduced nominal terms; a syntax with names and binding. Unification of nominal terms is decidable. This journal paper subsumes a conference version.

nomu-jv [pdf] [djvu] [bib] [DOI]
A New Approach to Abstract Syntax with Variable Binding Murdoch J. Gabbay and A.M. Pitts, Formal Aspects of Computing, Springer London, Volume 13, Numbers 3-5, July 2002 (special issue in honour of Rod Burstall).: We introduce nominal techniques, along with atoms-abstraction, the NEW quantifier, inductive datatypes of syntax-with-binding, and their inductive reasoning principles. A conference paper appeared in LICS'99.

newaas-jv [pdf] [djvu] [bib] [DOI]

top, journals, Book chapters, conferences, tech reports, abstracts, unpublished, thesis.

The lambda-calculus is nominal algebraic Murdoch J. Gabbay and Aad Mathijssen, in “Reasoning in Simple Type Theory, Festschrift in Honour of Peter B. Andrews on his 70th Birthday”, College Publications, December 2008, ISBN 978-1-904987-70-3.: We use nominal algebra to give a sound and complete axiomatisation of the lambda-calculus. This paper is subsumed by a journal version.

lamcna [pdf] [djvu] [bib] [amazon]
a-logic Murdoch J. Gabbay and Michael Gabbay, in “We Will Show Them: Essays in Honour of Dov Gabbay”, College Publications, October 2005, ISBN 978-1904987123.: We extend first-order logic with a predicate expressing the intensional property of a term “this is a variable symbol”. We axiomatise substition, object-level binding, and thus exhibit a finite first-order axiomatisation of the lambda-calculus. See also a related development.

[pdf] [djvu] [bib] [DBLP]
Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning, Michael Gabbay and Murdoch J. Gabbay, in “We Will Show Them: Essays in Honour of Dov Gabbay”, College Publications, October 2005, ISBN 978-1904987123.: We investigate "Restart" a natural deduction rule which reads "from A we may deduce B". This powerful rule by Dov Gabbay in the 1980s adds many theorems to intuitionistic logic; we investigate them and consider generalisations. This paper is not a hoax.
somfcg [pdf] [djvu] [bib] [DBLP]
The pi-calculus in FM Murdoch J. Gabbay, in “Thirty Five Years of Automating Mathematics”, Kluwer Applied Logic series, Volume 28, Pages 247-269, 2004, ISBN 978-1-4020-1656-5.: We discuss how to use nominal techniques to model name-generation, specifically in a process calculus, though the techniques use are probably more generally applicable.

picfm [pdf] [djvu] [bib] [amazon]
(Electronic versions differ in minor corrections from the printed version.)

top, journals, chapters, Conferences and workshops, tech reports, abstracts, unpublished, thesis.

Permissive-nominal logic Gilles Dowek, Murdoch J. Gabbay, Proceedings of the 12th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP'10), Pages: 165 - 176, 2010.: Permissive-Nominal Logic (PNL) is an extension of first-order logic where term-formers can bind names in their arguments.
This allows for direct axiomatisations with binders, such as the forall-quantifier of first-order logic itself and the lambda-binder of the lambda-calculus. This also allows us to finitely axiomatise arithmetic.
Like first- and higher-order logic and unlike other nominal logics, equality reasoning is not necessary to alpha-rename.
All this gives PNL much of the expressive power of higher-order logic, but terms, derivations and models of PNL are first-order in character, and the logic seems to strike a good balance between expressivity and simplicity.

pernl [bib] [djvu] [pdf] [DOI]
Closed nominal rewriting and efficiently computable nominal algebra equality Maribel Fernandez and Murdoch J. Gabbay, LFMTP 2010: We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality. This subclass includes specifications of lambda-calculus and first-order logic.

clonre [pdf] [djvu] [bib] [slides]
A simple class of Kripke-style models in which logic and computation have equal standing Michael J. Gabbay and Murdoch J. Gabbay, International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2010), 2010.: We present a sound and complete model of lambda-calculus reductions based on structures in- spired by modal logic (closely related to Kripke structures). Accordingly we can construct a logic which is sound and complete for the same models, and we identify lambda-terms with certain simple sentences (predicates) in this logic, by direct compositional translation. Reduction then becomes identified with logical entailment.

simcks [pdf] [djvu] [bib]
Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables Murdoch J. Gabbay and Dominic Mulligan, ACM International Conference Proceeding Series, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'09), Pages 64-73, 2009.: We translate between equality derivations in lambda-theories and equality derivations in permissive-nominal algebra theories. This connects logical reasoning over higher-order syntax, to logical reasoning over nominal terms.

unialt [pdf] [djvu] [bib] [DOI]
Permissive nominal terms and their unification Gilles Dowek, Murdoch J. Gabbay, and Dominic Mulligan, CILC, 24th Italian Conference on Computational Logic, 2009.: Permissive nominal terms resemble nominal terms, but using infinite and co-infinite sets of atoms gives a stronger theory of alpha-equivalence with ‘always fresh’ and ‘always alpha-rename’ properties familiar from first-and higher- order syntax. The notion of unifier is based on substitution alone, rather than on nominal terms' notion of substitution plus freshness conditions. Expressivity is not lost moving to the permissive case, and we demonstrate this with a simple translation between the nominal and the permissive-nominal settings.

perntu [bib] [djvu] [pdf]
Term sequent logic: Michael Gabbay and Murdoch J. Gabbay, Electronic Notes in Theoretical Computer Science, Volume 246, 3 August 2009, Pages 87-106, Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008); Term sequents apply notions of intro-rule and sequent presentation to terms, rather than predicates. We use this to build a logic for reasoning about the untyped lambda-calculus, similar to rewriting but with the power of first-order logic to deduce rewrites in the presence of assumptions.

tersl [pdf] [djvu] [bib] [DOI]

The ENTCS paper above subsumes a 15 page workshop paper of the same title, which appeared in the preproceedings of WFLP'08.

tersl (preproceedings) [pdf] [djvu] [bib]
One-and-a-halfth order terms: Curry-Howard and incomplete derivations Murdoch J. Gabbay and Dominic Mulligan, Lecture Notes in Computer Science, Springer, Volume 5110/2008, Pages 179-193, June 2008.: We apply nominal terms to propositions-as-types/proofs-as-terms in the presence of incomplete derivations. Atoms correspond with assumptions, unknowns correspond with incomplete parts of the derivation, and a freshness condition corresponds with the condition that an assumption will be discharged in an unknown part of the derivation.

curhid [pdf] [djvu] [bib] [DOI]
Nominal renaming sets Murdoch J. Gabbay and Martin Hofmann, Lecture Notes In Artificial Intelligence, Volume 5330, Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Pages 158 - 173, 2008.: Nominal renaming sets are like nominal sets, but they are based on a finitely-supported renaming action — a renaming is a function from atoms to atoms, not necessarily injective. This provides a convenient sets-based semantics with which to justify Higher-Order Abstract Syntax.

[pdf] [djvu] [bib] [DOI]
Two-level Lambda-calculus: Murdoch J. Gabbay and Dominic Mulligan, Electronic Notes in Theoretical Computer Science, Volume 246, 3 August 2009, Pages 107-129, Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008); The two-level lambda-calculus gives a functional operational semantics to nominal terms unknowns; the result is a lambda-calculus with capturing and capture-avoiding substitution are represented and nominal terms style alpha-equivalence for level 1 variables (atoms) in the presence of level 2 variables (unknowns).

twollc (ENTCS) [pdf] [djvu] [bib] [DOI]

The ENTCS paper above subsumes a 15 page workshop paper entitled Two-and-a-halfth order lambda-calculus, which appeared in the preproceedings of WFLP'08.

twoaah (preproceedings) [pdf] [djvu] [bib]
Substitution for Fraenkel-Mostowski Foundations Murdoch J. Gabbay and Michael Gabbay, Proceedings of the AISB Convention 2008, Pages 65-72.: We present a capture-avoiding substitution action defined in Fraenkel-Mostowski set theory on the entire sets universe. Substitution is commonly understood as an action on syntax (for example when building a logic or a lambda calculus) and thus as a prelude to, but not a part of, mathematical denotations. We show that it also has denotational realisation, as an operation on elements of a mathematical foundation.

subfmf [pdf] [djvu] [bib] [AISB online]
The lambda-context calculus Murdoch J. Gabbay and Stéphane Lengrand, Electronic Notes in Theoretical Computer Science, Volume 196, 22 January 2008, Pages 19-35, Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007).: We present a simple lambda-calculus whose syntax is populated by variables which behave like meta-variables. It can express both capture-avoiding and capturing substitution (instantiation).

lamcc [pdf] [djvu] [bib] [DOI]
a-logic with arrows Murdoch J. Gabbay and Michael J. Gabbay, Electronic Notes in Theoretical Computer Science, Volume 216, 4 July 2008, Pages 3-29, Proceedings of the 16th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2007).: This paper is subsumed by a journal version.
In a previous paper we discussed a-logic, a logic with a predicate ‘atom’ which is related to PROLOG's ‘isvar’. It identifies a term as a variable symbol. This provokes technical difficulties in the logic analogous to the difficulties giving a logical semantics to isvar. In this paper we give a completely overhauled proof-system, and a new denotational semantics, which resolve these technical issues by a directed notion of equality similar to a rewrite relation. The result is a greatly improved ability to axiomatise logic and computation.
See also the proceedings of the WFLP'07 workshop.

alwa [pdf] [djvu] [bib] [DOI]
A Formal Calculus for Informal Equality with Binding Murdoch J. Gabbay and Aad Mathijssen, Lecture Notes in Computer Science, Springer, Volume 4576/2007, Pages 162-176, 2007.: We describe Nominal Algebra, a logical calculus for reasoning which directly supports binding, based on nominal terms.

forcie [pdf] [djvu] [bib] [DOI]
Curry-style types for nominal terms Maribel Fernandez and Murdoch J. Gabbay, Lecture Notes in Computer Science, Springer Berlin, Volume 4502/2007, “Types for Proofs and Programs”, Pages 125-139.: Nominal terms are a representation of syntax-with-binding in the presence of explicit meta-variables and alpha-renaming. Making this consistent with a functional type system is non-trivial because the same meta-variable may appear in different contexts and under different binders, so when that meta-variable is instantiated the same variable name may be injected into different contexts of abstractions.

curstn [pdf] [djvu] [bib] [DOI]
One-and-a-halfth-order logic Murdoch J. Gabbay and Aad Mathijssen, Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP'06), Pages: 189 - 200, 2006.: We present a logic similar to first-order logic, but with predicate unknowns in nominal style. This permits schematic reasoning in the presence of ‘unknown predicates’ which may also occur under binders. We give both algebraic and sequent characterisations of derivability, prove their equivalence, prove cut-elimination of the sequent system, and show correctness with respect to first-order logic. See also the journal version.

oneaah [pdf] [djvu] [bib] [DOI]
Capture-avoiding Substitution as a Nominal Algebra Murdoch J. Gabbay and Aad Mathijssen, Lecture Notes in Computer Science, Springer, Volume 4281/2006, Theoretical Aspects of Computing - ICTAC 2006, Pages 198-212.: We give a detailed investigation of the fundamental operation which is capture-avoiding substitution, investigated from the point of view of Nominal Algebra. See also the journal version.

capasn [pdf] [djvu] [bib] [DOI]
SOS for higher-order processes MohammadReza Mousavi, Murdoch J. Gabbay and Michel Reniers, Lecture Notes in Computer Science, Springer Berlin, Volume 3653/2005, CONCUR 2005 – Concurrency Theory, Pages 308-322.: We propose promoted PANTH, a Structural Operational Semantics framework which extends Bernstein's propoted tyft/tyxt format, and for which a suitable notion of higher-order bisimulation is a congruence.

soshop [pdf] [djvu] [bib] [DOI]
(Here are slides on this, due to MohammadReza Mousavi.)
A NEW calculus of contexts Murdoch J. Gabbay Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP'05), Pages 94 - 105, 2005.: This is subsumed by a later journal paper.
We introduce a lambda-calculus in which context substitution (which does not avoid capture) has the same status as ordinary beta-reduction. We claim the calculus is expressive and can encode dynamic binding, objects, and interesting properties associated to partial evaluation. We prove meta-properties which include an applicative characterisation of contextual equivalence.

newcc [pdf] [djvu] [bib] [DOI]
Nominal Rewriting with Name Generation: abstraction vs. locality Maribel Fernandez, Murdoch J. Gabbay, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP'05), Pages 47 - 58, 2005.: We generalise and extend previous work on rewriting-with-variable-binding with a construct for name generation, and study its properties.

nomrng [pdf] [djvu] [bib] [DOI]
A Sequent Calculus for Nominal Logic Murdoch J. Gabbay and James Cheney, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, Pages 139 - 148, 2004.: We consider a sequent calculus for Nominal Logic, consider notions of Logic Programming for it, and give a translation of Miller and Tiu's FOLN.

seqcnl [pdf] [djvu] [bib] [DOI]
Nominal Rewriting Systems Maribel Fernandez, Murdoch J. Gabbay, Ian Mackie Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, ACM, Pages 108 - 119, 2004.: We generalise first-order rewriting with terms involving binding operations, using a nominal approach in which bound entities are explicitly named.

nomr [pdf] [djvu] [bib] [DOI]
FreshML: Programming with Binders Made Simple Mark R. Shinwell, Andrew M. Pitts and Murdoch J. Gabbay, ACM SIGPLAN Notices, Volume 38, Issue 9, Pages 263 - 274, September 2003.: frepbm [pdf] [djvu] [bib] [DOI]
Nominal Unification Christian Urban, Andrew Pitts, Murdoch J. Gabbay, Lecture Notes in Computer Science Springer, Volume 2803/2003, Computer Science Logic, 2003.: (See here for formal verification of the results in this paper, carried out by Urban using Isabelle.)

nomu [pdf] [djvu] [bib] [DOI]
FM-HOL, a higher-order theory of names Murdoch J. Gabbay, F. Kamareddine (Ed.) Thirty Five years of Automath, Heriot-Watt University, Edinburgh, Scotland, April 2002.: fmhotn [bib] [djvu] [ps.gz] [Proceedings]
Automating Fraenkel-Mostowski Syntax, Murdoch J. Gabbay, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2002), Pages, 60-70, August 2002. 15th International Conference on Theorem Proving in Higher Order Logics, 20-23 of August, 2002.: autfms [pdf] [djvu] [bib]
A Metalanguage for Programming with Bound Names Modulo Renaming Andrew M. Pitts and Murdoch J. Gabbay, Lecture Notes in Computer Science, Springer, Volume 1837/2000, Mathematics of Program Construction, 2000, Pages 230-255.: metpbn [pdf] [djvu] [bib] [DOI]
A New Approach to Abstract Syntax Involving Binders, Murdoch J. Gabbay and Andrew M. Pitts, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS'99), Pages 214-224, July 1999.: newaas [pdf, [djvu] [bib] [DOI]

top, journals, chapters, conferences, Technical reports, abstracts, unpublished, thesis.

An observation on support and freshness in nominal sets (technical report) Murdoch J. Gabbay, Heriot-Watt Technical report HW-MACS-TR-0077.: There are two natural ways of excluding an atom a in nominal techniques: we can either consider the sets X such that a is fresh for X, or we can consider the sets X such that a is fresh for every x ∈ X.
The statements of 'being fresh for all the elements of that set' and 'being fresh for a set' are not the same: it is not the case that ∀x ∈ X.a#x if and only if a#X. Both notions encode natural notions of 'fresh a'. In this paper, it is proved that these notions lead naturally to two categories that are isomorphic, so that in a suitable generalised sense they are the same.
The result is mathematically attractive and has an interesting reading: it is equivalent to add a fresh atom to the underlying universe, and to add a symbol to the meta-language referencing a fresh atom. Or to put it slightly differently: we prove the intuitively appealing but non-obvious fact that a fresh atom in the object-level is categorically isomorphic to a fresh atom in the meta-level.

obssfn-tr [pdf] [djvu] [bib] [HW-MACS-TR-0077]
Permissive nominal terms and their unification (technical report), Murdoch J. Gabbay, Heriot-Watt Technical report HW-MACS-TR-0062.: We consider permissive nominal terms, and their unification. Permissive nominal terms closely resemble nominal terms, but they recover these useful 'always fresh' and 'always alpha-rename' properties, familiar from first-and higher- order syntax. In the permissive world, freshness contexts are elided, and the notion of unifier is based on substitution alone, rather than on nominal terms' notion of substitution plus freshness conditions. We prove that expressivity is not lost moving to the permissive case and translate from nominal terms unification into permissive nominal terms unification.

perntu-tr [pdf] [djvu] [bib] [HW-MACS-TR-0062]
Permissive nominal terms (technical report) Murdoch J. Gabbay, INRIA technical report RR-6682.: We consider permissive nominal terms, and their unification. Permissive nominal terms closely resemble nominal terms, but they recover these useful 'always fresh' and 'always alpha-rename' properties, familiar from first-and higher- order syntax. In the permissive world, freshness contexts are elided, and the notion of unifier is based on substitution alone, rather than on nominal terms' notion of substitution plus freshness conditions.

RR-6682 [pdf] [djvu] [bib] [RR-6682]
Nominal renaming sets (technical report) Murdoch J. Gabbay, Heriot-Watt technical report HW-MACS-TR-0058.: This has been subsumed by my LPAR'08 paper with Hofmann.
We explore ‘nominal sets’ based on a renaming action (possibly non-injective functions on atoms) instead of the more usual permutation action. We find that Gabbay-Pitts atoms-abstraction coincides with functional abstraction, making a nice connection between the two notions of ‘abstract a variable’.

nomrs-tr [pdf] [djvu] [bib] [HW-MACS-TR-0058]
Nominal Algebra and the HSP theorem (technical report) Murdoch J. Gabbay and Aad Mathijssen, Heriot-Watt technical report HW-MACS-TR-0057.: This has been subsumed by a journal paper.
We prove the HSP (Homomorphism, Subalgebra, Product) theorem for Nominal Algebra, also known as Birkhoff's theorem.

nomahs-tr [pdf] [djvu] [bib] [HW-MACS-TR-0057]
Capture-avoiding Substitution as a Nominal Algebra (technical report) Murdoch J. Gabbay and Aad Mathijssen, Heriot-Watt technical report HW-MACS-TR-0053.: This has been subsumed by a journal paper.
Decidability and theory of models of a ‘nominal’ axiomatisation of capture-avoiding substitution.

capasn-tr [pdf] [djvu] [bib] [HW-MACS-TR-0053]
Nominal Algebra (technical report) Murdoch J. Gabbay and Aad Mathijssen, Heriot-Watt technical report HW-MACS-TR-0045.: A detailed treatment of the nominal algebra presented in our abstract in NWPT'06. This has been subsumed by a journal version.

noma-tr [pdf] [djvu] [bib] [HW-MACS-TR-0045]

top, journals, chapters, conferences, tech reports, Short (2-5 page) abstracts, unpublished, thesis.

Semantic nominal terms Murdoch J. Gabbay and Dominic Mulligan, TAASN'09.: We reconcile nominal atoms-abstraction with nominal terms. See the homepage of the Second International Workshop on Theory and Applications of Abstraction, Substitution and Naming (TAASN) 2009.

semnt-ea [pdf] [djvu] [bib]
Arbitrary Objects in Mathematics and Semantics Murdoch J. Gabbay and Michael Gabbay: In the Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics. A photo of Michael delivering the talk is online here.

arboms [pdf] [djvu] [bib]
Towards a Proof-Theoretic Approach to Plurality, Michael Gabbay and Murdoch J. Gabbay: In the Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics.

towpta [pdf] [djvu] [bib]
Nominal Algebra Murdoch J. Gabbay and Aad Mathijssen, in the 18th Nordic Workshop on Programming Theory, Reykjavík, Iceland, October 18-20, 2006.: We describe Nominal Algebra, an algebraic system which can directly encode systems-with-binding without using functions. Slides of the accompanying talk are here, and a paper is here.

noma-nwpt [pdf] [djvu] [bib]
Nominal SOS MohammadReza Mousavi, Michel A. Reniers and Murdoch J. Gabbay, in in the 18th Nordic Workshop on Programming Theory, Reykjavík, Iceland, October 18-20, 2006.: We describe Nominal Structured Operational Semantics, a framework for specifying operational semantics within which proofs of congruence are carried out ‘once and for all’.

nomsos-nwpt [pdf] [djvu] [bib]
Nominal Sets, Equivariance Reasoning, and Variable Binding Murdoch J. Gabbay: A prose account of my talk at MLG'02 in Kinosaki, Japan.

nomser [pdf] [djvu] [bib]

top, journals, chapters, conferences, tech reports, abstracts, Unpublished (for now), thesis.

Fresh Graphs Murdoch J. Gabbay: We introduce a new notion of ‘Fresh Graph’, this is a graph with binding, to model behaviour with dynamic allocation. We will finish this Real Soon Now.

freg

top, journals, chapters, conferences, tech reports, abstracts, unpublished, Thesis.

A Theory of Inductive Definitions with Alpha-Equivalence Murdoch J. Gabbay: PhD Thesis, Cambridge University, 2001.
thesis [pdf] [djvu]

Papers

Murdoch James Gabbay