Papers

Mindmap viewer

Scroll down for pdf and BibTeX of my papers. Click above for a flash-based graphical presentation. Download the open source software used to create this map here. See also Murdoch J. Gabbay on DBLP (not always up-to-date).
If you don’t know my work, here’s a brief technical overview: I do mathematical computer science with an emphasis on first- and higher-order logics, sets, semantics, and mathematical foundations. Most of my papers concern the application of nominal techniques to problems in the semantics of logic, programming and computation.
You might also be interested in some notes on writing an academic paper.

journal — chapter — conference — tech report — abstract — pending — thesis

2012, Log. Jour. IGPL

metvil

Meta-variables as infinite lists in nominal terms unifiation and rewriting, journal version. Murdoch J. Gabbay, Logic Journal of the IGPL, 2012, in press.

Nominal terms unknowns modelled concretely as infinite lists of distinct atoms. Theorems simplify and many become trivial corollaries of equivariance.

2012, TOCL

pernl-jv

Permissive-nominal logic, journal version. Gilles Dowek and Murdoch J. Gabbay, Transactions on Computational Logic, 2012, in press.

First-order logic with term-formers that can bind names. So we can axiomatise things like forall or lambda, or finitely axiomatise arithmetic. This gives PNL much of the expressive power of higher-order logic: but terms, derivations and models of PNL are first-order and the logic seems to strike a good balance between expressivity and simplicity. In brief, PNL is obtained by adding universal quantification to nominal algebra. But, to make that work we needed to invent permission sets. This is a journal version of the conference paper.

2011, HOWARD-60

stodfo

Stone duality for first-order logic: a nominal approach to logic and topology. Murdoch J. Gabbay, Howard Barringer Festschrift, 2011.

Stone duality for first-order logic. Open predicates map to open sets. No valuations. See also the ancestor of this paper, Stone duality for nominal Boolean algebras with NEW. This version of the paper differs slightly from the version that appeared in the Festschrift in the correction of some small typos and errors.

2011, MSCS

twolns

Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables. Murdoch J. Gabbay, Mathematical Structures in Computer Science, Volume 21, Issue 5, Pages 997-1033, 2011..

A “nominal” denotational semantics for meta-variables. Consider λx.t. Here x is an object-variable and t is a meta-variable. Nominal sets gave x a denotational reality and this turned out to be fruitful. This paper does the same for t. The slogan: “meta-variables using sets with a permutation action”.
The version on this webpage includes corrections relative to the publisher’s version.

2011, BSL

fountl

Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Murdoch J. Gabbay, Bulletin of Symbolic Logic, Volume 17, Number 2, June 2011, Pages 161-229.

A survey and update paper describing nominal techniques, with specific application to nominal abstract syntax. A sequel to this paper is Nominal terms and nominal logics.

2010, Log. Jour. IGPL

perntu-jv

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, Volume 8, Number 6, 2010, Pages 769-822.

A problem I have with nominal terms is that you can’t quotient them by alpha-equivalence. If you want something ‘nominal’, but closer to first-order syntax, then permissive nominal terms could be an answer.
This journal paper extends the conference version and technical report and includes some elements from another conference paper.
The version linked to below (pdf, djvu) includes minor corrections with respect to the published version (DOI).

2010, I&C

curhif-jv

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.

Types-as-propositions, incomplete (nominal) terms as incomplete derivations. That is, the “variables” of nominal terms become “holes” in first-order logic derivations. A freshness condition becomes a promise that an assumption will be discharged.
This journal paper expands on the conference version.

2010, I&C

lamcce

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.

The lambda-context calculus is a multi-level lambda-calculus, generalising a two-level lambda-calculus with an infinite hierarchy of variables such that higher level variables behave like meta-variables with respect to lower level variables. It can express both capture-avoiding and capturing substitution (instantiation), explicit substitutions, references, and more.
An extended version of our LFMTP’07 paper.

2010, JLC

nomalc

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.

It’s easy to write down axioms for the lambda-calculus in nominal algebra—but do you know those axioms are right? We prove completeness of axioms for alpha-beta-(eta) equivalence. It’s mostly obvious, but not entirely so, and the proofs aren’t trivial. This subsumes a previous book chapter.

2009, JLC

nomuae

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.

Nominal Algebra, a logic for equational reasoning over nominal sets, which uses nominal terms. Think: “algebra with term-formers that can bind”.
This paper subsumes conference versions in WOLLIC’07 and NWPT’06, and a 2006 technical report, and is followed by Nominal terms, nominal logics.
Many of the papers applying nominal algebra were in print before the journal paper. You might be interested in Capture-avoiding substitution as a nominal algebra, One-and-a-halfth order logic, Nominal algebra and the HSP theorem, and A nominal axiomatisation of the lambda-calculus.

2009, TCS

stusun

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.

Nominal sets contain names and alpha-equivalence, so what about defining a capture-avoiding substitution action for them? We give a notion of “replace a by y in x” where x and y are any two sets.
This subsumes the AISB’08 paper, and is followed by Freshness and name-restriction in sets of traces with names.

2009, JLC

nomahs

Nominal Algebra and the HSP theorem. Murdoch J. Gabbay, Journal of Logic and Computation, Volume 19, Number 2, April 2009, pages 341-367.

It’s not obvious that Nominal Algebra is a pure equational logic, because of freshness conditions. E.g. η-conversion (eta-conversion) looks like this: a#X⊢λa.(Xa)=X. This is a conditional equality.
So I proved an HSPA theorem for Nominal Algebra—any model of a Nominal Algebra theory is part of a quotient of a product of atoms-abstractions of free models. This places limits on the complexity of models, and puts a precise measure on the notion of equality of nominal algebra: making things equal, putting things into tuples, and forming atoms-abstracton.

2008, ENTCS

alwa-jv

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.

2008, Formal Asp. Comp.

capasn-jv

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.

Nominal algebra makes it easy to write axioms for capture-avoiding substitution—or does it? Consider the choices: do you want b[a↦X]=b or a#Z⊢Z[a↦X]=Z? Do you want Z[a↦a]=Z or not? In this paper we write down various plausible axioms and prove senses in which they are correct.
This is a journal version of our ICTAC’06 paper.

2008, JLC

oneaah-jv

One-and-a-halfth-order logic. Murdoch J. Gabbay and Aad Mathijssen, Journal of Logic and Computation, August, 2008, Volume 18, Pages 521-562.

Nominal algebra makes it fairly easy to write axioms for first-order logic. This gives us is ‘first-order logic, with incomplete predicates’—so we can represent reasoning schematically over predicates (which might occur inside binders).
For instance, we can represent the schematic assertion “if a does not occur in φ then φ implies ∀a.φ” and its derivation as “a#X⊢X⊃∀a.X” and corresponding schematic derivations. We give algebraic and sequent characterisations, and show correctness with respect to first-order logic.
This subsumes the PPDP’06 conference paper.

2007, I&C

nomr-jv

Nominal Rewriting. Maribel Fernández and Murdoch J. Gabbay, Information and Computation, Volume 205, Issue 6, June 2007, Pages 917-965.

Rewriting on nominal terms. An example: a#X⊢λa.(Xa)→X (eta-contraction). By doing this, nominal techniques changed from being about syntax-with-binding to being about specifications-with-binding. We also consider criteria for confluence.
This is the journal version of our PPDP’04 paper, and is followed by Nominal universal algebra. You might also be interested in Closed nominal rewriting and efficiently computable nominal algebra equality.

2007, ENTCS

hienr

Hierarchical nominal terms and their theory of rewriting. Murdoch J. Gabbay, Electronic Notes in Theoretical Computer Science, Volume 174, Issue 5, June 2007, Pages 37-52.

So nominal terms have two levels of variable. But that just means we’ve internalised the meta-level once. What if we do this repeatedly until we reach a fixedpoint? We build a theory of rewriting on nominal terms with an infinite hierarchy of variables. We examine 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 my LFMTP’06 workshop paper.

2007, I&C

genmn

A General Mathematics of Names. Murdoch J. Gabbay, Information and Computation, Volume 205, Issue 7, July 2007, Pages 982-1011.

Nominal sets as presented e.g. in my first journal paper have an atoms-abstraction operation generalising alpha-equivalence. In this paper we generalise this to infinite simultaneous alpha-equivalence. The underlying technical ‘trick’ is to interpret ‘small’ as ‘well-orderable’. So sets of atoms are small when they can be well-ordered. (So of course, we drop the nominal ‘finite support’ property and take instead a generalised nominal ‘well-orderable support’ property.)

2007, JAL

frelog

Fresh Logic. Murdoch J. Gabbay, Journal of Applied Logic, Volume 5, Issue 2, June 2007, Pages 356-387.

The first proof-theory for the NEW quantifier, with sound and complete semantics. See also a subsequently written LICS conference paper with Cheney.
Yes, I know the LICS conference paper came out three years earlier—it’s amazing how long it takes for a journal paper to get into print.

2004, TCS

nomu-jv

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, which extend first-order terms with term-formers that can bind. Unification of nominal terms is decidable and has most general unifiers. This journal paper subsumes a conference version. The next step up in abstraction from nominal terms is their permissive variant.

2004, Formal Asp. Comp.

newaas-jv

A New Approach to Abstract Syntax with Variable Binding. Murdoch J. Gabbay and Andrew M. Pitts, Formal Aspects of Computing, Springer London, Volume 13, Numbers 3-5, July 2002 (special issue in honour of Rod Burstall).

The paper that started it all, at least for me. We introduce nominal sets, atoms-abstraction, the NEW quantifier, and nominal abstract syntax (inductive datatypes of syntax-with-binding) and their inductive reasoning principles.
A conference paper appeared in LICS’99.

journal — book chapter — conference — tech report — abstract — pending — thesis

2012, Hndb’k of Philos. Log.

nomtnl

Nominal terms and nominal logics: from foundations to meta-mathematics. Murdoch J. Gabbay, Handbook of Philosophical Logic (2nd ed), Volume 17, 2012, in press.

A survey and update chapter describing a journey from (permissive-)nominal sets, via nominal terms, rewriting and algebra, to permissive-nominal logic and a finite first-order nominal axiomatisation of arithmetic: in short, mathematical logic based on nominal terms. See also Foundations of nominal techniques.

2008, College Pub.

lamcna

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. Subsumed by a journal version.

2008, College Pub.

alogic

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.

2008, College Pub.

somfcg

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.

2004, Kluwer App. Log.

picfm

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. (Electronic versions differ in minor corrections from the printed version.)

journal — chapter — conferences and workshops — tech report — abstract — pending — thesis

LFMTP 2011

nomhss

Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets. Murdoch Gabbay and Dominic P. Mulligan, 6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, Electronic Proceedings in Theoretical Computer Science, volume 71, pages 58-75.

Henkin-style models of the lambda-calculus in nominal sets. No Tarski-style valuations; instead we use nominal substitution algebras. The title of the paper as it appeared in the pre-proceedings was: “Semantics for functions of the simply-typed lambda-calculus with nominal sets”.

FCT 2011

pritnt

Principal types for nominal theories. Elliot Fairweather, Maribel Fernández, and Murdoch Gabbay, 8th International Symposium on Fundamentals of Computation Theory, 2011.

Rank 1 polymorphic types for nominal rewriting and algebra. So you want to type rules like beta- or eta-conversion over nominal terms? This paper describes one way to do it.

CALCO 2011

stodnb

Stone duality for nominal Boolean algebras with New. Murdoch J. Gabbay, Tadeusz Litak, and Daniela Petrisan, 4th Conference on Algebra and Coalgebra in Computer Science (CALCO 2011), 2011.

The “new” quantifier is the canonical name-generation/name-restriction operator for predicates on the “nominal” model of names and binding. We give a sets representation theorem and extend this to a Stone duality. See also the subsequent Stone duality for first-order logic.

FOSSACS 2011

frenrs

Freshness and name-restriction in sets of traces with names. Murdoch J. Gabbay and Vincenzo Ciancia, Foundations of software science and computation structures, 14th International Conference (FOSSACS 2011), 2011.

A concrete sets model of name-generation/name-restriction using a relative of Gabbay-Pitts atoms-abstraction. The technical innovation is the notion of a positive subset of a nominal set.

PPDP 2010

pernl

Permissive-nominal logic. Gilles Dowek and Murdoch J. Gabbay, Proceedings of the 12th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP’10), pages 165-176, 2010.

(See also the journal version.) First-order logic with term-formers that can bind names. So we can axiomatise things like forall or lambda, or finitely axiomatise arithmetic. This gives PNL much of the expressive power of higher-order logic: but terms, derivations and models of PNL are first-order and the logic seems to strike a good balance between expressivity and simplicity. In brief, PNL is obtained by adding universal quantification to nominal algebra. But, to make that work we needed to invent permission sets.

LFMTP 2010

clonre

Closed nominal rewriting and efficiently computable nominal algebra equality. Maribel Fernández and Murdoch J. Gabbay, Proceedings of the 5th International Workshop on Logical Frameworks and Meta-Languages (LFMTP 2010), Electronic Proceedings in Theoretical Computer Science, volume 34, pages 37-51.

We ask how nominal algebra and nominal rewriting relate, giving a 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.

LPAR 2010

simcks

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).

We present a sound and complete model of lambda-calculus reductions based on structures inspired 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.

LFMTP 2009

unialt

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. In brief: higher-order reasoning injects into nominal algebra.

CILC 2009

perntu

Permissive nominal terms and their unification. Gilles Dowek, Murdoch J. Gabbay, and Dominic Mulligan, 24th Italian Conference on Computational Logic (CILC 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.

WFLP 2008

tersl

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.
This ENTCS paper subsumes a 15 page workshop paper of the same title, which appeared in the preproceedings of WFLP’08.

WOLLIC 2008

curhid

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.

LPAR 2008

nomrs

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.

WFLP 2008

twollc

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).
This ENTCS paper subsumes a 15 page workshop paper entitled “Two-and-a-halfth order lambda-calculus”, which appeared in the preproceedings of WFLP’08.

AISB 2008

subfmf

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.

LFMTP 2007

lamcc

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).

WFLP 2007

alwa

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.

WOLLIC 2007

forcie

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. See also applications Capture-avoiding substitution as a nominal algebra and One-and-a-halfth order logic in 2006, and the later journal version.

TYPES 2006

curstn

Curry-style types for nominal terms. Maribel Fernández and Murdoch J. Gabbay, Lecture Notes in Computer Science, Springer Berlin, Volume 4502/2007, “Types for Proofs and Programs (TYPES 2006)”, 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.

PPDP 2006

oneaah

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 2006), 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.

ICTAC 2006

capasn

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.

CONCUR 2005

soshop

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. (Slidesedinburgh.pdf by MohammadReza Mousavi.)

PPDP 2005

newcc

A NEW calculus of contexts. Murdoch J. Gabbay, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP 2005), Pages 94 – 105, 2005..

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.
This is subsumed by a later journal paper.

PPDP 2005

nomrng

Nominal Rewriting with Name Generation: abstraction vs. locality. Maribel Fernández, Murdoch J. Gabbay, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP 2005), Pages 47 – 58, 2005.

We generalise and extend previous work on rewriting-with-variable-binding with name generation/restriction, and study its properties.

LICS 2004

seqcnl

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.

PPDP 2004

nomr

Nominal Rewriting Systems. Maribel Fernández, 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.

ICFP 2003

frepbm

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.

FreshML enriches ML with Gabbay-Pitts nominal atoms-abstraction.

CSL 2003

nomu

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.)

35 yrs Automath

fmhotn

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..

A generalisation of Fraenkel-Mostowski techniques to deal with infinite support and infinite atoms-abstraction. Largely but not completely superseded by a general mathematics of names.

TPHOLS 2002

autfms

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.

MPC 2000

metpbn

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, pages 230-255, 2000..

LICS 1999

newaas

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.

My first conference paper. See also the journal version.

journal — chapter — conference — tech report — abstract — pending — thesis

HW-MACS-TR-0077

obssfn-tr

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.

HW-MACS-TR-0062

perntu-tr

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.

INRIA RR-6682

pernt-tr

Permissive nominal terms (technical report). Murdoch J. Gabbay, INRIA technical report RR-6682.

HW-MACS-TR-0058

nomrs-tr

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’.

HW-MACS-TR-0057

nomahs

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.

HW-MACS-TR-0053

capasn-tr

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.

HW-MACS-TR-0045

noma-tr

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.

journal — chapter — conference — tech report — short (2-5 page) abstracts — pending — thesis

TAASN 2009

semnt-ea

Semantic nominal terms. Murdoch J. Gabbay and Dominic Mulligan, Second International Workshop on Theory and Applications of Abstraction, Substitution, and Naming (TAASN 2009).

We reconcile nominal atoms-abstraction with nominal terms. This idea is developed more fully in a journal paper on two-level nominal sets.

Arché 2008

arboms

Arbitrary Objects in Mathematics and Semantics. Murdoch J. Gabbay and Michael Gabbay, Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics, February 28-March 1, 2008.

A photo of Michael delivering the talk is online here.

Arché 2008

towpta

Towards a Proof-Theoretic Approach to Plurality. Michael Gabbay and Murdoch J. Gabbay, Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics, February 28-March 1, 2008.

NWPT 2006

noma-nwpt

Nominal Algebra. Murdoch J. Gabbay and Aad Mathijssen, 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.

NWPT 2006

nomsos-nwpt

Nominal SOS. MohammadReza Mousavi, Michel A. Reniers and Murdoch J. Gabbay, 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’.

MLG 2002

nomser

Nominal Sets, Equivariance Reasoning, and Variable Binding. Murdoch J. Gabbay, MLG 2002.

A prose account of my talk at MLG’02 in Kinosaki, Japan.

journal — chapter — conference — tech report — abstract — pending — thesis

arXiv 2011

nomsbf-arxiv

From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions. Gilles Dowek and Murdoch J. Gabbay, arXiv, November 2011.

We translate PNL to HOL (permissive-nominal logic to higher-order logic). Notably, this involved turning a nominal atoms-abstraction into a total function.

2012, JSL

finisn

Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free. Murdoch J. Gabbay, Accepted (*), Journal of Symbolic Logic.

Moving between permissive-nominal (infinitely-supported) and nominal (finitely-supported) models, with applications to permissive-nominal algebra completeness and permissive-nominal logic completeness. A lot of cool stuff playing with nominal sets. (*) Accepted by referees, pending authorisation by the JSL’s editorial committee.

freg

Fresh Graphs. Murdoch J. Gabbay, will finish Real Soon Now.

We introduce a new notion of ‘Fresh Graph’, this is a graph with binding, to model behaviour with dynamic allocation.

journal — chapter — conference — tech report — abstract — pending — thesis

Camb. 2001

thesis

A Theory of Inductive Definitions with Alpha-Equivalence. Murdoch J. Gabbay, PhD Thesis, Cambridge University, 2001. .

If you’re interested in this you might also like my recent survey of the foundations on nominal techniques