Scroll down for pdf, djvu (what's that?), and BibTeX of my papers.
Murdoch J. Gabbay on DBLP.

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

gabbay:stusun
Murdoch J. Gabbay A study of substitution, using nominal techniques and Fraenkel-Mostowski sets. A journal version of my AISB'08 paper, with two subtitution actions and full proofs. We investigate two capture-avoiding substitutions action on Fraenkel-Mostowski set theory, in the sense of capasn-jv. 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 investigate it as an operation on a mathematical foundation, specifically, Fraenkel-Mostowski set theory.
gabbay:nomahs
Murdoch J. Gabbay Nominal Algebra and the HSP theorem, pending publication in the Journal of Logic and Computation. Nominal Algebra is a version of universal algebra based on nominal terms — thus, an equivariant system with support for freshness, binding, and permutation, as promoted by me and Pitts, and later by me and Mathijssen. The HSP theorem for universal algebra states that any algebra is the homomorphic image of subalgebra of a product of free algebras; think of this as ‘the fundamental theorem of arithmetic’ (any number is the product of prime numbers), but for algebras. Mathematicians like to prove this kind of result; it puts a limit the number of ways that a widget can be constructed, and thus on the widget's mathematical behaviour. In this paper we prove an HSP theorem for nominal algebra. The twist in the tale is that we must also assume atoms-abstraction, a construct characteristic of nominal techniques. The proofs are also rather beautiful, if you like nominal sets.
gabbay:alwa-jv
Murdoch J. Gabbay and Michael J. Gabbay a-logic with arrows (journal version), in ENTCS. DOI 10.1016/j.entcs.2008.06.031. The journal version of our WFLP'07 paper, with an improved proof-system. 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.
gabbay:capasn-jv
Murdoch J. Gabbay and Aad Mathijssen Capture-avoiding Substitution as a Nominal Algebra, in Formal Aspects of Computing. also available online in DOI 10.1007/s00165-007-0056-1. We investigate capture-avoiding substitution using Nominal Algebra. This is a journal version of a conference paper, with improved proofs.
gabbay:oneaah-jv
Murdoch J. Gabbay and Aad Mathijssen One-and-a-halfth-order logic, in the Journal of Logic and Computation. DOI 10.1093/logcom/exm064. 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.
A conference version is here.
gabbay:nomr-jv
Maribel Fernandez and Murdoch J. Gabbay Nominal Rewriting, in Information and Computation, Volume 205, Issue 6, June 2007, Pages 917-965, DOI 10.1016/j.ic.2006.12.002. The journal version of our PPDP'04 paper. Nominal rewriting is rewriting in the presence of meta-level unknowns, object-level variable symbols, and alpha-equivalence, but nothing else. Substitution of terms for unknowns remains first-order; no capture-avoidance.
gabbay:hienr
Murdoch J. Gabbay Hierarchical nominal terms and their theory of rewriting, in Electronic Notes in Theoretical Computer Science, Volume 174, Issue 5, 2 June 2007, Pages 37-52, DOI 10.1016/j.entcs.2007.01.017. 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.

A workshop version appeared in proceedings of LFMTP'06 here.

gabbay:genmn
Murdoch J. Gabbay A General Mathematics of Names, Information and Computation, Volume 205, Issue 7, July 2007, Pages 982-1011, DOI 10.1016/j.ic.2006.10.010. We present Fraenkel-Mostowski Generalised set theory. This generalises Fraenkel-Mostowski set theory (FM sets) to a theory which can interpret infinitary syntax (with infinitely many different names, which would violate the finite support property assumed in FM sets.
gabbay:frelog
Murdoch J. Gabbay, Fresh Logic, Journal of Applied Logic, Volume 5, Issue 2, June 2007, Pages 356-387, DOI 10.1016/j.jal.2005.10.012. We give cut-free sequent and natural deduction logics which include a NEW-quantifier, freshness predicate, and swapping.
gabbay:nomu-jv
Christian Urban, Andrew M.Pitts and Murdoch J.Gabbay, Nominal Unification, Theoretical Computer Science, Volume 323, Issues 1-3, 14 September 2004, Pages 473-497, DOI 10.1016/j.tcs.2004.06.016. (The conference paper is below.)
gabbay:picfm
Murdoch J. Gabbay, The pi-calculus in FM, In Thirty Five Years of Automating Mathematics, edited by Fairouz Kamareddine, Kluwer Applied Logic series. Volume 28. Pages 247-269. November 2003. ISBN 1-4020-1656-5.
[abstract] [bib] [djvu] [djvu (crop)] [pdf] [pdf (crop)]
(Electronic versions differ in minor corrections from the printed version.)
gabbay:newaas-jv
Murdoch J. Gabbay and A.M. Pitts, A New Approach to Abstract Syntax with Variable Binding, Formal Aspects of Computing, special issue in honour of Rod Burstall, 2001. (This is an extended and revised version of gabbay:newaas.)

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

gabbay:lamcna
Murdoch J. Gabbay and Aad Mathijssen The lambda-calculus is nominal algebraic, in the Festschrift in Honour of Peter B. Andrews on his 70th Birthday. We use nominal algebra to give a sound and complete axiomatisation of the lambda-calculus.
gabbay:alogic
Murdoch J. Gabbay and Michael Gabbay a-logic, in the Dov Gabbay 60th birthday festschrift. We examine a simple but powerful extension of first-order logic with a predicate expressing the intensional properties of a term "this is a variable symbol". We apply it to axiomatise object-level explicit substition, object-level binding, and thus exhibit a finite first-order axiomatisation of the lambda-calculus.
gabbay:somfcg
Michael Gabbay and Murdoch J. Gabbay Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning, in the Dov Gabbay 60th birthday festschrift. 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.

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

gabbay:nomrs
Murdoch J. Gabbay and Martin Hofmann Nominal renaming sets, in LPAR'08. We discuss nominal renaming sets. These are like nominal sets, but 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.
gabbay:twoaah
Murdoch J. Gabbay and Dominic Mulligan Two-and-a-halfth order lambda-calculus, in WFLP'08. We introduce two-and-a-halfth order lambda-calculus. This introduces a functional operational semantics to the ‘unknowns’ of nominal terms; the result is a lambda-calculus in which both capturing and capture-avoiding substitution are represented, with a full (nominal terms style) theory of alpha-equivalence for level 1 variables (atoms) in the presence of level 2 variables (unknowns).
You might also like to look at the lambda-context calculus.
gabbay:tersl
Michael Gabbay and Murdoch J. Gabbay Term sequent logic, in WFLP'08. We introduce term sequents which apply notions of intro-rule and sequent presentation for terms. 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.
gabbay:curhid
Murdoch J. Gabbay and Dominic Mulligan One-and-a-halfth order terms: Curry-Howard for incomplete derivations, in WOLLIC'08. 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.
gabbay:subfmf
Murdoch J. Gabbay and Michael Gabbay Substitution for Fraenkel-Mostowski Foundations, in the AISB symposium on computing and philosophy. We present a capture-avoiding substitution action on Fraenkel-Mostowski set theory. 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 reality as an operation on a mathematical foundation.
gabbay:lamcc
Murdoch J. Gabbay and Stéphane Lengrand The lambda-context calculus, in LFMTP'07, DOI j.entcs.2007.09.015; also online at ENTCS volume 196. 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).
gabbay:alwa
Murdoch J. Gabbay and Michael J. Gabbay a-logic with arrows, in WFLP'2007; see also the proceedings of the entire workshop and the full journal paper.
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.
gabbay:forcie
Murdoch J. Gabbay and Aad Mathijssen A Formal Calculus for Informal Equality with Binding, in WOLLIC'2007. DOI 10.1007/978-3-540-73445-1_12. We describe Nominal Algebra, a logical calculus for reasoning which directly supports binding.
gabbay:nomsos-nwpt
MohammadReza Mousavi, Michel A. Reniers and Murdoch J. Gabbay Nominal SOS, in NWPT'06. We describe Nominal Structured Operational Semantics, a framework for specifying operational semantics within which proofs of congruence are carried out ‘once and for all’.
gabbay:noma-nwpt
Murdoch J. Gabbay and Aad Mathijssen Nominal Algebra, in NWPT'06. 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.
gabbay:curstn
Maribel Fernandez and Murdoch J. Gabbay Curry-style types for nominal terms, In TYPES'06. 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.
gabbay:oneaah
Murdoch J. Gabbay and Aad Mathijssen One-and-a-halfth-order logic, in PPDP 2006. DOI 10.1145/1140335.1140359. 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.
gabbay:capasn
Murdoch J. Gabbay and Aad Mathijssen Capture-avoiding Substitution as a Nominal Algebra, in ICTAC 2006. We give a detailed investigation of the fundamental operation which is capture-avoiding substitution, investigated from the point of view of Nominal Algebra.
gabbay:soshop
MohammadReza Mousavi, Murdoch J. Gabbay and Michel Reniers SOS for higher-order processes, in CONCUR'2005. 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.
[abstract] [bib] [djvu] [djvu (crop)] [pdf] [pdf (crop)]
(Here are slides on this, due to MohammadReza Mousavi.)
gabbay:newcc
Murdoch J. Gabbay A NEW calculus of contexts, in PPDP'2005, DOI 10.1145/1069774.1069783. 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.
gabbay:nomrng
Maribel Fernandez, Murdoch J. Gabbay Nominal Rewriting with Name Generation: abstraction vs. locality, in PPDP'2005. We generalise and extend previous work on rewriting-with-variable-binding with a construct for name generation, and study its properties.
gabbay:seqcnl
Murdoch J. Gabbay and James Cheney A Sequent Calculus for Nominal Logic, DOI 10.1109/LICS.2004.6. In LICS'04. 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.
gabbay:nomr
Maribel Fernandez, Murdoch J. Gabbay, Ian Mackie Nominal Rewriting, in PPDP'04. We generalise first-order rewriting with terms involving binding operations, using a nominal approach in which bound entities are explicitly named.
gabbay:frepbm
M. R. Shinwell, A.M. Pitts and M.J.Gabbay, FreshML: Programming with Binders Made Simple, In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden, pages 263-274 (ACM Press, 2003).
gabbay:nomser
Murdoch J. Gabbay, Nominal Sets, Equivariance Reasoning, and Variable Binding, A brief prose account of my talk at MLG'02 in Kinosaki, Japan.
gabbay:nomu
Christian Urban, Andrew Pitts, Murdoch J. Gabbay, Nominal Unification, M.Baaz (Ed.), Computer Science Logic and 8th Kurt Godel Colloquium (CSL'03 & KGC), Vienna, Austria. Proccedings. Lecture Notes in Computer Science, Volume 2803, pages 513-527 (Springer-Verlag, 2003). (See here for formal verification of the results in this paper, carried out by Urban using Isabelle.)
gabbay:fmhhotn
Murdoch J. Gabbay, FM-HOL, a higher-order theory of names, In F. Kamareddine (Ed.) Workshop on Thirty Five years of Automath, Informal Proceedings, Heriot-Watt University, Edinburgh, Scotland, April 2002.
gabbay:autfms
Murdoch J. Gabbay, Automating Fraenkel-Mostowski Syntax, In TPHOLs 2002, 15th International Conference on Theorem Proving in Higher Order Logics, 20-23 of August, 2002.
gabbay:metpbn
A. M. Pitts and Murdoch J. Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming. In R. Backhouse and J. N. Oliveira (Eds), Mathematics of Programme Construction, 5th International Conference, MPC2000, Ponte de Lima, Portugal, July 2000. Proceedings. Lecture Notes in Computer Science, Volume 1837 (Springer-Verlag, 2000), pages 230-255.
gabbay:newaas
M.J. Gabbay and A.M. Pitts, A New Approach to Abstract Syntax Involving Binders, In Proceedings 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 1999, (IEEE Computer Society Press, 1999) pp 214-224. On Citeseer.

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

gabbay:nomrs-tr
Murdoch J. Gabbay Nominal renaming sets (technical report), Technical report HW-MACS-TR-0058. 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’.
gabbay:nomahs-tr
Murdoch J. Gabbay and Aad Mathijssen Nominal Algebra and the HSP theorem (technical report), Technical report HW-MACS-TR-0057. We prove the HSP (Homomorphism, Subalgebra, Product) theorem for Nominal Algebra, also known as Birkhoff's theorem.
gabbay:capasn-tr
Murdoch J. Gabbay and Aad Mathijssen Capture-avoiding Substitution as a Nominal Algebra (technical report). Technical report HW-MACS-TR-0053 studies the decidability and theory of models of a ‘nominal’ axiomatisation of capture-avoiding substitution.
gabbay:noma-tr
Murdoch J. Gabbay and Aad Mathijssen Nominal Algebra (technical report), Technical report HW-MACS-TR-0045 which includes a detailed treatment of proofs in nominal algebra.

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

gabbay:arboms
Murdoch J. Gabbay and Michael Gabbay Arbitrary Objects in Mathematics and Semantics, 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.
gabbay:towptp
Michael Gabbay and Murdoch J. Gabbay Towards a Proof-Theoretic Approach to Plurality, in the Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics.

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

gabbay:setfnt
Murdoch J. Gabbay The sets foundations of nominal techniques. A survey and update paper describing a view of the foundations of nominal techniques. I welcome comments.
[pdf]
gabbay:nomaua
Murdoch J. Gabbay and Aad Mathijssen Nominal algebra: a universal algebra with names and binding, a journal version of our WOLLIC'07 paper. We describe Nominal Algebra, a logical calculus for reasoning which directly supports binding. I welcome comments.
gabbay:freg
Murdoch J. Gabbay, Fresh Graphs, 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.

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

gabbay:thesis
Murdoch J. Gabbay, A Theory of Inductive Definitions with Alpha-Equivalence, PhD Thesis, Cambridge University, 2001. Supervised by Andrew Pitts.