There is something fascinating about science. One gets such wholesale returns of conjecture out of such a trifling investment of fact.

# Papers

Click for short view

Algebras of UTxO blockchains
(algub:
bib
URI
pdf)

Murdoch J. Gabbay,

*Mathematical Structures in Computer Science, January 2022, Firstview*.Algebras of UTxO blockchains
algubbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Mathematical Structures in Computer Science, January 2022, Firstview* We condense the theory of UTxO blockchains down to a simple and compact set of four type equations (Idealised EUTxO), and to an algebraic characterisation (abstract chunk systems), and exhibit an adjoint pair of functors between them. This gives a novel account of the essential mathematical structures underlying blockchain technology, such as Bitcoin.

Karl Marx and the blockchain
(karmb:
bib
URI
pdf)

Devraj Basu and Murdoch J. Gabbay,

*In Media, Technology and Education in a Post-Truth Society: From Fake News, Datafication and Mass Surveillance to the Death of Trust, 8 July 2021*.Karl Marx and the blockchain
karmbbibtex
publisherURI
localpdf

Devraj Basu and Murdoch J. Gabbay,

*In Media, Technology and Education in a Post-Truth Society: From Fake News, Datafication and Mass Surveillance to the Death of Trust, 8 July 2021* We consider blockchain technology from a historical, social, and economic perspective, through a lens of the economic theories of Karl Marx.

UTxO- vs account-based smart contract blockchain programming paradigms
(utxabs:
bib
URI
pdf)

Lars Brünjes and Murdoch J. Gabbay,

*Accepted to the 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2020)*.UTxO- vs account-based smart contract blockchain programming paradigms
utxabsbibtex
publisherURI
localpdf

Lars Brünjes and Murdoch J. Gabbay,

*Accepted to the 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2020)* We implement two versions of a simple but illustrative smart contract: one in Solidity on the Ethereum blockchain platform, and one in Plutus on the Cardano platform, with annotated code excerpts and with source code attached. We prove some simple but novel results about observational equivalence and conclude with a wide-ranging and detailed discussion in the light of the examples, mathematical model, and mathematical results so far.

Equivariant ZFA and the foundations of nominal techniques
(equzfn:
bib
URI
pdf)

Murdoch J. Gabbay,

*Journal of Logic and Computation, Volume 30, Issue 2, March 2020, Pages 525-548*.Equivariant ZFA and the foundations of nominal techniques
equzfnbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Journal of Logic and Computation, Volume 30, Issue 2, March 2020, Pages 525-548* A new take on the foundations of nominal techniques.

The language of Stratified Sets is confluent and strongly normalising
(lanssc:
bib
URI
pdf)

Murdoch J. Gabbay,

*Logical Methods in Computer Science, May 2018, Volume 14, Issue 2, Article Number 12*.The language of Stratified Sets is confluent and strongly normalising
lansscbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Logical Methods in Computer Science, May 2018, Volume 14, Issue 2, Article Number 12* Quine's stratification condition viewed from the perspective of the theory of rewriting.

Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness
(repdul:
bib
URI
pdf)

Murdoch J. Gabbay and Michael J. Gabbay,

*Annals of Pure and Applied Logic, March 2017, Volume 168, Pages 501-621*.Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness
repdulbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Michael J. Gabbay,

*Annals of Pure and Applied Logic, March 2017, Volume 168, Pages 501-621* Everything you wanted to know about semantics of the lambda-calculus using nominal techniques.

Semantics out of context: nominal absolute denotations for first-order logic and computation
(semooc:
bib
URI
pdf)

Murdoch J. Gabbay,

*Journal of the ACM, June 2016, Volume 6, Issue 3, Pages 1-66*.Semantics out of context: nominal absolute denotations for first-order logic and computation
semoocbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Journal of the ACM, June 2016, Volume 6, Issue 3, Pages 1-66* Everything you wanted to know about semantics of first-order logic in nominal sets, topologies, and lattices. A sister paper is Stone duality for first-order logic. Available also on ArXiv.

Imaginary groups: lazy monoids and reversible computation
(imaglm:
bib
URI
pdf)

Murdoch J. Gabbay and Peter Kropholler,

*Mathematical Structures in Computer Science, October 2013, Volume 23, Issue 5*.Imaginary groups: lazy monoids and reversible computation
imaglmbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Peter Kropholler,

*Mathematical Structures in Computer Science, October 2013, Volume 23, Issue 5* A duality between partially ordered groups and an (apparently novel) category of partially ordered monoids and lazy homomorphisms between them. Every monoid can be lazily injected into a group. Reading a monoid as an abstract notion of computation (or at least, of composition), this construction shows how to add reversibility.

Denotation of contextual modal type theory (CMTT): syntax and metaprogramming
(dencmt:
bib
URI
pdf)

Murdoch J. Gabbay and Aleksandar Nanevski,

*Journal of Applied Logic, Volume 11, Issue 1, March 2013, Pages 1-29*.Denotation of contextual modal type theory (CMTT): syntax and metaprogramming
dencmtbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Aleksandar Nanevski,

*Journal of Applied Logic, Volume 11, Issue 1, March 2013, Pages 1-29* A denotation for CMTT. I wanted to understand this for years, and now we have an answer!

Quantifiers in logic and proof-search using permissive-nominal terms and sets
(qualps:
bib
URI
pdf)

Murdoch J. Gabbay and Claus-Peter Wirth,

*Journal of Logic Computation, online 23 February 2013, advance access*.Quantifiers in logic and proof-search using permissive-nominal terms and sets
qualpsbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Claus-Peter Wirth,

*Journal of Logic Computation, online 23 February 2013, advance access* Nominal terms used to model the γ- and δ-rules controlling quantifiers in reductive proof search.

PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
(pnlthf:
bib
URI
pdf)

Gilles Dowek and Murdoch J. Gabbay,

*Theoretical Computer Science, Volume 451, 14 September 2012, Pages 38-69*.PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
pnlthfbibtex
publisherURI
localpdf

Gilles Dowek and Murdoch J. Gabbay,

*Theoretical Computer Science, Volume 451, 14 September 2012, Pages 38-69* We translate PNL to HOL (permissive-nominal logic to higher-order logic). Notably, this involved turning a nominal atoms-abstraction into a total function.

Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
(finisn:
bib
URI
pdf)

Murdoch J. Gabbay,

*Journal of Symbolic Logic, September 2012, Volume 77, Number 3*.Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
finisnbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Journal of Symbolic Logic, September 2012, Volume 77, Number 3* Moving between permissive-nominal (infinitely-supported) and nominal (finitely-supported) models, with applications to permissive-nominal algebra completeness and permissive-nominal logic completeness. Cool stuff playing with nominal sets.

Meta-variables as infinite lists in nominal terms unification and rewriting (journal version)
(metvil:
bib
URI
pdf)

Murdoch J. Gabbay,

*Logic Journal of the IGPL, December 2012, Volume 20, Issue 6*.Meta-variables as infinite lists in nominal terms unification and rewriting (journal version)
metvilbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Logic Journal of the IGPL, December 2012, Volume 20, Issue 6* Nominal terms unknowns modelled concretely as infinite lists of distinct atoms. Theorems simplify and many even become immediate corollaries of equivariance.

Permissive-nominal logic (journal version)
(pernl-jv:
bib
URI
pdf)

Gilles Dowek and Murdoch J. Gabbay,

*Transactions on Computational Logic, July 2012, Volume 17, Number 3*.Permissive-nominal logic (journal version)
pernl-jvbibtex
publisherURI
localpdf

Gilles Dowek and Murdoch J. Gabbay,

*Transactions on Computational Logic, July 2012, Volume 17, Number 3* 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":#pernl.
Stone duality for first-order logic: a nominal approach to logic and topology
(stodfo:
bib
URI
pdf)

Murdoch J. Gabbay,

*Howard Barringer Festschrift, 2011*.Stone duality for first-order logic: a nominal approach to logic and topology
stodfobibtex
publisherURI
localpdf

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 from the version that appeared in the Festschrift in the correction of some small typos and errors.

Unity in nominal equational reasoning: The algebra of equality on nominal sets
(uniner:
bib
URI
pdf)

Murdoch J. Gabbay,

*Journal of Applied Logic, June 2012, Volume 10, Issue 2, Pages, 199-217*.Unity in nominal equational reasoning: The algebra of equality on nominal sets
uninerbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Journal of Applied Logic, June 2012, Volume 10, Issue 2, Pages, 199-217* An exhaustive analysis of the design choices involved in nominal equational / equality / algebra logic over nominal sets.

Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
(twolns:
bib
URI
pdf)

Murdoch J. Gabbay,

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

Murdoch J. Gabbay,

*Mathematical Structures in Computer Science, Volume 21, Issue 5, Pages 997-1033, 2011* A nominal denotational semantics for meta-variables. Nominal techniques have already given semantics to variables; in this paper we show how they can do the same for meta-variables. The version on this webpage includes corrections.

Foundations of nominal techniques: logic and semantics of variables in abstract syntax
(fountl:
bib
URI
pdf)

Murdoch J. Gabbay,

*Bulletin of Symbolic Logic, Volume 17, Number 2, June 2011, Pages 161-229*.Foundations of nominal techniques: logic and semantics of variables in abstract syntax
fountlbibtex
publisherURI
localpdf

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.

Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
(perntu-jv:
bib
URI
pdf)

Gilles Dowek, Murdoch J. Gabbay, and Dominic Mulligan,

*Logic Journal of the IGPL, Volume 8, Number 6, 2010, Pages 769-822*.Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
perntu-jvbibtex
publisherURI
localpdf

Gilles Dowek, Murdoch J. Gabbay, and Dominic Mulligan,

*Logic Journal of the IGPL, Volume 8, Number 6, 2010, Pages 769-822* You cannot quotient nominal terms by alpha-equivalence, but you can quotient permissive nominal terms. This journal paper extends the conference version and technical report and includes some elements from another conference paper. My version includes minor corrections to the published version.

Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
(curhif-jv:
bib
URI
pdf)

Murdoch J. Gabbay and Dominic Mulligan,

*Information and Computation, Volume 208, Issue 3, March 2010, Pages 230-258*.Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
curhif-jvbibtex
publisherURI
localpdf

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

This journal paper expands on the conference version.

*will*be discharged.This journal paper expands on the conference version.

The lambda-context calculus (extended version)
(lamcce:
bib
URI
pdf)

Murdoch J. Gabbay and Stéphane Lengrand,

*Information and Computation, Volume 207, Issue 12, December 2009, Pages 1369-1400*.The lambda-context calculus (extended version)
lamccebibtex
publisherURI
localpdf

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

An extended version of our LFMTP'07 paper.

*and*capturing substitution (instantiation), explicit substitutions, references, and more.An extended version of our LFMTP'07 paper.

A nominal axiomatisation of the lambda-calculus
(nomalc:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*Journal of Logic and Computation, Volume 20, Number 2, pages 501-531, April 2010*.A nominal axiomatisation of the lambda-calculus
nomalcbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Aad Mathijssen,

*Journal of Logic and Computation, Volume 20, Number 2, pages 501-531, April 2010* We can write axioms for the lambda-calculus in nominal algebra—but do we know those axioms are right? We prove completeness of axioms for alpha-beta-(eta) equivalence. This subsumes a previous book chapter.

Nominal universal algebra: equational logic with names and binding
(nomuae:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*Journal of Logic and Computation, Volume 19, Number 6, December 2009, pages 1455-1508*.Nominal universal algebra: equational logic with names and binding
nomuaebibtex
publisherURI
localpdf

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 WOLLIC07 and NWPT06, 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

Many of the papers applying nominal algebra were in print before the journal paper. You might be interested in

A study of substitution, using nominal techniques and Fraenkel-Mostowski sets
(stusun:
bib
URI
pdf)

Murdoch J. Gabbay,

*Theoretical Computer Science, Volume 410, Issues 12-13, 17 March 2009, Pages 1159-1189*.A study of substitution, using nominal techniques and Fraenkel-Mostowski sets
stusunbibtex
publisherURI
localpdf

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

This subsumes the AISB08 paper, and is followed by Freshness and name-restriction in sets of traces with names.

*a*by*y*in*x*" where*x*and*y*are any two sets.This subsumes the AISB08 paper, and is followed by Freshness and name-restriction in sets of traces with names.

Nominal Algebra and the HSP theorem
(nomahs:
bib
URI
pdf)

Murdoch J. Gabbay,

*Journal of Logic and Computation, Volume 19, Number 2, April 2009, pages 341-367*.Nominal Algebra and the HSP theorem
nomahsbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Journal of Logic and Computation, Volume 19, Number 2, April 2009, pages 341-367* It is 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. The HSPA theorem for Nominal Algebra asserts that any model of a Nominal Algebra theory is part of a quotient of a product of atoms-abstractions of free models. This limits 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.

a-logic with arrows (journal version)
(alwa-jv:
bib
URI
pdf)

Murdoch J. Gabbay and Michael J. Gabbay,

*Electronic Notes in Theoretical Computer Science, Volume 216, 4 July 2008, Pages 3-29*.a-logic with arrows (journal version)
alwa-jvbibtex
publisherURI
localpdf

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 WFLP07 paper, with an improved proof-system.

Capture-avoiding Substitution as a Nominal Algebra
(capasn-jv:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*Formal Aspects of Computing, Volume 20, Numbers 4-5, July, 2008, Pages 451-479*.Capture-avoiding Substitution as a Nominal Algebra
capasn-jvbibtex
publisherURI
localpdf

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

This is a journal version of our ICTAC06 paper.

**prove**senses in which they are correct.This is a journal version of our ICTAC06 paper.

One-and-a-halfth-order logic
(oneaah-jv:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*Journal of Logic and Computation, August, 2008, Volume 18, Pages 521-562*.One-and-a-halfth-order logic
oneaah-jvbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Aad Mathijssen,

*Journal of Logic and Computation, August, 2008, Volume 18, Pages 521-562* A logic of schematic reasoning based on nominal algebra. 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 PPDP06 conference paper.

Nominal Rewriting
(nomr-jv:
bib
URI
pdf)

Maribel Fernández and Murdoch J. Gabbay,

*Information and Computation, Volume 205, Issue 6, June 2007, Pages 917-965*.Nominal Rewriting
nomr-jvbibtex
publisherURI
localpdf

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). Nominal techniques changed from being about syntax-with-binding to being about specifications-with-binding. We also consider criteria for confluence. See the PPDP04 conference paper and Nominal universal algebra and Closed nominal rewriting and efficiently computable nominal algebra equality.

Hierarchical nominal terms and their theory of rewriting
(hienr:
bib
URI
pdf)

Murdoch J. Gabbay,

*Electronic Notes in Theoretical Computer Science, Volume 174, Issue 5, June 2007, Pages 37-52*.Hierarchical nominal terms and their theory of rewriting
hienrbibtex
publisherURI
localpdf

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 have 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 LFMTP06 workshop paper.

This is a revised and expanded version of my LFMTP06 workshop paper.

A General Mathematics of Names
(genmn:
bib
URI
pdf)

Murdoch J. Gabbay,

*Information and Computation, Volume 205, Issue 7, July 2007, Pages 982-1011*.A General Mathematics of Names
genmnbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Information and Computation, Volume 205, Issue 7, July 2007, Pages 982-1011* Nominal sets as introduced here have an atoms-abstraction operation generalising alpha-equivalence. In this paper we consider infinite simultaneous alpha-equivalence. The trick is to interpret small as well-orderable.

Fresh Logic
(frelog:
bib
URI
pdf)

Murdoch J. Gabbay,

*Journal of Applied Logic, Volume 5, Issue 2, June 2007, Pages 356-387*.Fresh Logic
frelogbibtex
publisherURI
localpdf

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 the subsequent LICS paper. The conference paper came into print three years earlier, though it was written later.

Nominal Unification
(nomu-jv:
bib
URI
pdf)

Christian Urban, Andrew M. Pitts and Murdoch J. Gabbay,

*Theoretical Computer Science, Volume 323, Issues 1-3, 14 September 2004, Pages 473-497*.Nominal Unification
nomu-jvbibtex
publisherURI
localpdf

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.

A New Approach to Abstract Syntax with Variable Binding
(newaas-jv:
bib
URI
pdf)

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)*.A New Approach to Abstract Syntax with Variable Binding
newaas-jvbibtex
publisherURI
localpdf

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. See also the conference version in LICS99.

Nominal terms and nominal logics: from foundations to meta-mathematics
(nomtnl:
bib
URI
pdf)

Murdoch J. Gabbay,

*Handbook of Philosophical Logic (2nd ed), Volume 17, 2013*.Nominal terms and nominal logics: from foundations to meta-mathematics
nomtnlbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Handbook of Philosophical Logic (2nd ed), Volume 17, 2013* 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. See also Foundations of nominal techniques.

The lambda-calculus is nominal algebraic
(lamcna:
bib
URI
pdf)

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*.The lambda-calculus is nominal algebraic
lamcnabibtex
publisherURI
localpdf

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.

a-logic
(alogic:
bib
URI
pdf)

Murdoch J. Gabbay and Michael Gabbay,

*in "We Will Show Them: Essays in Honour of Dov Gabbay", College Publications, October 2005, ISBN 978-1904987123*.a-logic
alogicbibtex
publisherURI
localpdf

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.

Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning
(somfcg:
bib
URI
pdf)

Michael Gabbay and Murdoch J. Gabbay,

*in "We Will Show Them: Essays in Honour of Dov Gabbay", College Publications, October 2005, ISBN 978-1904987123.*.Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning
somfcgbibtex
publisherURI
localpdf

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 is not a hoax.

The pi-calculus in FM
(picfm:
bib
URI
pdf)

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*.The pi-calculus in FM
picfmbibtex
publisherURI
localpdf

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

Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes
(leannt:
bib
URI
pdf)

Murdoch J. Gabbay, Dan R. Ghica and Daniela Petrișan,

*24th EACSL Annual Conference on Computer Science Logic (CSL 2015)*.Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes
leanntbibtex
publisherURI
localpdf

Murdoch J. Gabbay, Dan R. Ghica and Daniela Petrișan,

*24th EACSL Annual Conference on Computer Science Logic (CSL 2015)* Split "νa.t" as "〈a t a〉". If that looks simple, try "〈a〈b ab a〉b〉" or "〈a〈b abb〉".

Game semantics in the nominal model
(gamsnm:
bib
URI
pdf)

Murdoch Gabbay and Dan Ghica,

*Twenty-eighth Conference on the Mathematical Foundations of Programming Semantics (MFPS), 2012*.Game semantics in the nominal model
gamsnmbibtex
publisherURI
localpdf

Murdoch Gabbay and Dan Ghica,

*Twenty-eighth Conference on the Mathematical Foundations of Programming Semantics (MFPS), 2012* Nominal semantics used to model and generalise pointer sequences, using a nice new idea of

*nominal coabstraction*. The result: an expression of game semantics using nominal-style atoms.
Nominal semantics for predicate logic
(nomspl:
bib
URI
pdf)

Gilles Dowek and Murdoch Gabbay,

*Ninth Italian Convention on Computational Logic (CILC), 2012*.Nominal semantics for predicate logic
nomsplbibtex
publisherURI
localpdf

Gilles Dowek and Murdoch Gabbay,

*Ninth Italian Convention on Computational Logic (CILC), 2012* Universal lattice properties used to specify top, meet, and forall as instances of a single notion of

*fresh-finite limit*.
Game semantics in the nominal model
(gamsnm:
bib
URI
pdf)

Murdoch Gabbay and Dan Ghica,

*Twenty-eighth Conference on the Mathematical Foundations of Programming Semantics (MFPS), 2012*.Game semantics in the nominal model
gamsnmbibtex
publisherURI
localpdf

Murdoch Gabbay and Dan Ghica,

*Twenty-eighth Conference on the Mathematical Foundations of Programming Semantics (MFPS), 2012* Nominal semantics used to model and generalise pointer sequences, using a nice new idea of

*nominal coabstraction*. The result: an expression of game semantics using nominal-style atoms.
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
(nomhss:
bib
URI
pdf)

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*.Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
nomhssbibtex
publisherURI
localpdf

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 in the pre-proceedings was

*Semantics for functions of the simply-typed lambda-calculus with nominal sets*.
Principal types for nominal theories
(pritnt:
bib
URI
pdf)

Elliot Fairweather, Maribel Fernández, and Murdoch Gabbay,

*8th International Symposium on Fundamentals of Computation Theory, 2011*.Principal types for nominal theories
pritntbibtex
publisherURI
localpdf

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.

Stone duality for nominal Boolean algebras with New
(stodnb:
bib
URI
pdf)

Murdoch J. Gabbay, Tadeusz Litak, and Daniela Petrisan,

*4th Conference on Algebra and Coalgebra in Computer Science (CALCO 2011), 2011*.Stone duality for nominal Boolean algebras with New
stodnbbibtex
publisherURI
localpdf

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 Stone-type duality. See also the subsequent Stone duality for first-order logic.

Freshness and name-restriction in sets of traces with names
(frenrs:
bib
URI
pdf)

Murdoch J. Gabbay and Vincenzo Ciancia,

*Foundations of software science and computation structures, 14th International Conference (FOSSACS 2011), 2011*.Freshness and name-restriction in sets of traces with names
frenrsbibtex
publisherURI
localpdf

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.
Permissive-nominal logic
(pernl:
bib
URI
pdf)

Gilles Dowek and Murdoch J. Gabbay,

*Proceedings of the 12th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP10), pages 165-176, 2010*.Permissive-nominal logic
pernlbibtex
publisherURI
localpdf

Gilles Dowek and Murdoch J. Gabbay,

*Proceedings of the 12th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP10), pages 165-176, 2010* First-order logic with binding term-formers. We can axiomatise

*forall*or*lambda*, and finitely axiomatise arithmetic. PNL has much of the expressive power of higher-order logic but terms, derivations and models of PNL are first-order. PNL is nominal algebra" + quantification over nominal unknowns. See also the journal version.
Closed nominal rewriting and efficiently computable nominal algebra equality
(clonre:
bib
URI
pdf)

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*.Closed nominal rewriting and efficiently computable nominal algebra equality
clonrebibtex
publisherURI
localpdf

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 relate nominal algebra and rewriting, with 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, which includes specifications of lambda-calculus and first-order logic.

A simple class of Kripke-style models in which logic and computation have equal standing
(simcks:
bib
URI
pdf)

Michael J. Gabbay and Murdoch J. Gabbay,

*International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2010)*.A simple class of Kripke-style models in which logic and computation have equal standing
simcksbibtex
publisherURI
localpdf

Michael J. Gabbay and Murdoch J. Gabbay,

*International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2010)* A sound and complete model of lambda-calculus reductions in structures related to Kripke structures. We construct a logic for the models and identify lambda-terms with predicates by direct compositional translation. Reduction becomes logical entailment.

Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables
(unialt:
bib
URI
pdf)

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 (LFMTP09), Pages 64-73, 2009*.Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables
unialtbibtex
publisherURI
localpdf

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 (LFMTP09), Pages 64-73, 2009* We translate between equality derivations in lambda-theories and equality derivations in permissive-nominal algebra theories. This connects reasoning over higher-order syntax to reasoning over nominal terms.

Permissive nominal terms and their unification
(perntu:
bib
URI
pdf)

Gilles Dowek, Murdoch J. Gabbay, and Dominic Mulligan,

*24th Italian Conference on Computational Logic (CILC 2009)*.Permissive nominal terms and their unification
perntubibtex
publisherURI
localpdf

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. We get ‘always fresh’ and ‘always alpha-rename’ properties familiar from first-and higher- order syntax but absent from nominal terms. See also the journal version

Term sequent logic
(tersl:
bib
URI
pdf)

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 sequent logic
terslbibtex
publisherURI
localpdf

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*are sequents for terms instead of predicates. We build lambda-calculus reductions, similar to rewriting but with structure corresponding to proof-theory. This subsumes a 15 page workshop paper of the same title which appeared in the preproceedings of WFLP08.

One-and-a-halfth order terms: Curry-Howard and incomplete derivations
(curhid:
bib
URI
pdf)

Murdoch J. Gabbay and Dominic Mulligan,

*Lecture Notes in Computer Science, Springer, Volume 5110/2008, Pages 179-193, June 2008*.One-and-a-halfth order terms: Curry-Howard and incomplete derivations
curhidbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Dominic Mulligan,

*Lecture Notes in Computer Science, Springer, Volume 5110/2008, Pages 179-193, June 2008* Nominal terms give Curry-Howard for schematic derivations. Atoms correspond with assumptions, unknowns correspond with schematic parts of the derivation, freshness conditions corresponds with the condition that an assumption

*will*be discharged (even if the schema does not specify how).
Nominal renaming sets
(nomrs:
bib
URI
pdf)

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
nomrsbibtex
publisherURI
localpdf

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.

Two-level Lambda-calculus
(twollc:
bib
URI
pdf)

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)*.Two-level Lambda-calculus
twollcbibtex
publisherURI
localpdf

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

This ENTCS paper subsumes a 15 page workshop paper entitled "Two-and-a-halfth order lambda-calculus", which appeared in the preproceedings of WFLP08.

Substitution for Fraenkel-Mostowski Foundations
(subfmf:
bib
URI
pdf)

Murdoch J. Gabbay and Michael Gabbay,

*Proceedings of the AISB Convention 2008, Pages 65-72*.Substitution for Fraenkel-Mostowski Foundations
subfmfbibtex
publisherURI
localpdf

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.

The lambda-context calculus
(lamcc:
bib
URI
pdf)

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).*.The lambda-context calculus
lamccbibtex
publisherURI
localpdf

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).
a-logic with arrows
(alwa:
bib
URI
pdf)

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).*.a-logic with arrows
alwabibtex
publisherURI
localpdf

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).* Subsumed by the journal version. A previous paper on

*a-logic*includes a predicate ‘atom’ related to ‘isvar&rsquo from PROLOG; to identify a term as a variable symbol. We give an overhauled proof-system, and a new denotational semantics, which use a*directed*notion of equality similar to a rewrite relation. We get improved ability to axiomatise logic and computation. See also the proceedings of the WFLP07 workshop.
A Formal Calculus for Informal Equality with Binding
(forcie:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*Lecture Notes in Computer Science, Springer, Volume 4576/2007, Pages 162-176, 2007*.A Formal Calculus for Informal Equality with Binding
forciebibtex
publisherURI
localpdf

Murdoch J. Gabbay and Aad Mathijssen,

*Lecture Notes in Computer Science, Springer, Volume 4576/2007, Pages 162-176, 2007* Nominal Algebra, a logic for equality reasoning with freshness and 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.

Curry-style types for nominal terms
(curstn:
bib
URI
pdf)

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*.Curry-style types for nominal terms
curstnbibtex
publisherURI
localpdf

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.

One-and-a-halfth-order logic
(oneaah:
bib
URI
pdf)

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*.One-and-a-halfth-order logic
oneaahbibtex
publisherURI
localpdf

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* A logic for schematic first-order reasoning; unknown predicates are nominal unknowns in the sense of nominal terms and may occur under binders. We characterise derivability using nominal algebra and using sequents, prove equivalence, cut-elimination, and correctness. See the journal version.

Capture-avoiding Substitution as a Nominal Algebra
(capasn:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*Lecture Notes in Computer Science, Springer, Volume 4281/2006, Theoretical Aspects of Computing - ICTAC 2006, Pages 198-212*.Capture-avoiding Substitution as a Nominal Algebra
capasnbibtex
publisherURI
localpdf

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.

SOS for higher-order processes
(soshop:
bib
URI
pdf)

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*.SOS for higher-order processes
soshopbibtex
publisherURI
localpdf

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* Promoted PANTH is a Structural Operational Semantics framework extends tyft/tyxt, for which a notion of higher-order bisimulation is a congruence. (Slides by MohammadReza Mousavi.)

A NEW calculus of contexts
(newcc:
bib
URI
pdf)

Murdoch J. Gabbay,

*Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP 2005), Pages 94 - 105, 2005*.A NEW calculus of contexts
newccbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP 2005), Pages 94 - 105, 2005* Subsumed by a later journal paper. A lambda-calculus with context substitution (which does not avoid capture) alongside ordinary beta-reduction. It can encode dynamic binding, objects, and interesting properties associated to partial evaluation. Meta-properties include an applicative characterisation of contextual equivalence.

Nominal Rewriting with Name Generation: abstraction vs. locality
(nomrng:
bib
URI
pdf)

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*.Nominal Rewriting with Name Generation: abstraction vs. locality
nomrngbibtex
publisherURI
localpdf

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.

A Sequent Calculus for Nominal Logic
(seqcnl:
bib
URI
pdf)

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*.A Sequent Calculus for Nominal Logic
seqcnlbibtex
publisherURI
localpdf

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* A sequent calculus for Nominal Logic. We consider notions of Logic Programming in it and give a translation of Miller and Tiu's FOLN.

Nominal Rewriting Systems
(nomr:
bib
URI
pdf)

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*.Nominal Rewriting Systems
nomrbibtex
publisherURI
localpdf

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.

FreshML: Programming with Binders Made Simple
(frepbm:
bib
URI
pdf)

Mark R. Shinwell, Andrew M. Pitts and Murdoch J. Gabbay,

*ACM SIGPLAN Notices, Volume 38, Issue 9, Pages 263 - 274, September 2003*.FreshML: Programming with Binders Made Simple
frepbmbibtex
publisherURI
localpdf

Mark R. Shinwell, Andrew M. Pitts and Murdoch J. Gabbay,

*ACM SIGPLAN Notices, Volume 38, Issue 9, Pages 263 - 274, September 2003* ML enriched with Gabbay-Pitts atoms-abstraction and nominal name-generation and pattern-matching.

Nominal Unification
(nomu:
bib
URI
pdf)

Christian Urban, Andrew Pitts, Murdoch J. Gabbay,

*Lecture Notes in Computer Science, Springer, Volume 2803/2003, Computer Science Logic, 2003*.
FM-HOL, a higher-order theory of names
(fmhotn:
bib
URI
pdf)

Murdoch J. Gabbay,

*F. Kamareddine (Ed.) Thirty Five years of Automath, Heriot-Watt University, Edinburgh, Scotland, April 2002.*.FM-HOL, a higher-order theory of names
fmhotnbibtex
publisherURI
localpdf

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.

Automating Fraenkel-Mostowski Syntax
(autfms:
bib
URI
pdf)

Murdoch J. Gabbay,

*Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2002), pages, 60-70, August 2002*.Automating Fraenkel-Mostowski Syntax
autfmsbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2002), pages, 60-70, August 2002*
A Metalanguage for Programming with Bound Names Modulo Renaming
(metpbn:
bib
URI
pdf)

Andrew M. Pitts and Murdoch J. Gabbay,

*Lecture Notes in Computer Science, Springer, Volume 1837/2000, Mathematics of Program Construction, pages 230-255, 2000.*.A Metalanguage for Programming with Bound Names Modulo Renaming
metpbnbibtex
publisherURI
localpdf

Andrew M. Pitts and Murdoch J. Gabbay,

*Lecture Notes in Computer Science, Springer, Volume 1837/2000, Mathematics of Program Construction, pages 230-255, 2000.*
A New Approach to Abstract Syntax Involving Binders
(newaas:
bib
URI
pdf)

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*.A New Approach to Abstract Syntax Involving Binders
newaasbibtex
publisherURI
localpdf

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.

Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
(densmc:
bib
URI
pdf)

Murdoch J. Gabbay and Alexander Nanevski,

*arXiv 1202.0904, 2012*.Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
densmcbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Alexander Nanevski,

*arXiv 1202.0904, 2012* Subsumed by this journal paper.

From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions
(nomsbf-arxiv:
bib
URI
pdf)

Gilles Dowek and Murdoch J. Gabbay,

*arXiv, November 2011*.From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions
nomsbf-arxivbibtex
publisherURI
localpdf

Gilles Dowek and Murdoch J. Gabbay,

*arXiv, November 2011* Subsumed by this journal paper.

An observation on support and freshness in nominal sets (technical report)
(obssfn-tr:
bib
URI
pdf)

Murdoch J. Gabbay,

*Heriot-Watt Technical report HW-MACS-TR-0077*.An observation on support and freshness in nominal sets (technical report)
obssfn-trbibtex
publisherURI
localpdf

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 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. We show these lead to isomorphic categories. This can be read as saying that a fresh atom in the object-level is categorically isomorphic to a fresh atom in the meta-level.

Permissive nominal terms and their unification (technical report)
(perntu-tr:
bib
URI
pdf)

Murdoch J. Gabbay,

*Heriot-Watt Technical report HW-MACS-TR-0062*.Permissive nominal terms and their unification (technical report)
perntu-trbibtex
publisherURI
localpdf

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.

Permissive nominal terms (technical report)
(pernt-tr:
bib
URI
pdf)

Murdoch J. Gabbay,

*INRIA technical report RR-6682*.Permissive nominal terms (technical report)
pernt-trbibtex
publisherURI
localpdf

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.

Nominal renaming sets (technical report)
(nomrs-tr:
bib
URI
pdf)

Murdoch J. Gabbay,

*Heriot-Watt technical report HW-MACS-TR-0058*.Nominal renaming sets (technical report)
nomrs-trbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Heriot-Watt technical report HW-MACS-TR-0058* Subsumed by my LPAR08 paper with Martin Hofmann. Nominal sets based on a renaming action (possibly non-injective functions on atoms) instead of the more usual permutation action.

Nominal Algebra and the HSP theorem (technical report)
(nomahs:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*Heriot-Watt technical report HW-MACS-TR-0057*.Nominal Algebra and the HSP theorem (technical report)
nomahsbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Aad Mathijssen,

*Heriot-Watt technical report HW-MACS-TR-0057* Subsumed by a journal paper. We prove the HSP (Homomorphism, Subalgebra, Product) theorem for Nominal Algebra, also known as Birkhoffs theorem.

Capture-avoiding Substitution as a Nominal Algebra (technical report)
(capasn-tr:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*Heriot-Watt technical report HW-MACS-TR-0053*.Capture-avoiding Substitution as a Nominal Algebra (technical report)
capasn-trbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Aad Mathijssen,

*Heriot-Watt technical report HW-MACS-TR-0053* Subsumed by a journal paper. Decidability and theory of models of a nominal algebra axiomatisation of capture-avoiding substitution.

Nominal Algebra (technical report)
(noma-tr:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*Heriot-Watt technical report HW-MACS-TR-0045*.Nominal Algebra (technical report)
noma-trbibtex
publisherURI
localpdf

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 NWPT06":#noma-nwpt. Subsumed by "a journal version":#noma-jv.

Quantifier rules in reductive proof using nominal semantics
(quarrp-ea:
bib
URI
pdf)

Murdoch J. Gabbay,

*Automated reasoning workshop (ARW 2012)*.Quantifier rules in reductive proof using nominal semantics
quarrp-eabibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Automated reasoning workshop (ARW 2012)* We consider liberalised delta-rules in proof-search, and give them a nominal algebraic semantics.

Metamathematics based on nominal terms and nominal logic
(metbnt-ea:
bib
URI
pdf)

Murdoch J. Gabbay,

*Automated reasoning workshop (ARW 2011)*.Metamathematics based on nominal terms and nominal logic
metbnt-eabibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*Automated reasoning workshop (ARW 2011)* We sketch what theorem-proving might look like if it were based on nominal terms. This eventually evolved into "Nominal terms and nominal logics":#nomtnl.

Semantic nominal terms
(semnt-ea:
bib
URI
pdf)

Murdoch J. Gabbay and Dominic Mulligan,

*Second International Workshop on Theory and Applications of Abstraction, Substitution, and Naming (TAASN 2009)*.Semantic nominal terms
semnt-eabibtex
publisherURI
localpdf

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. See the journal paper on "two-level nominal sets":#twolns.

Arbitrary Objects in Mathematics and Semantics
(arboms:
bib
URI
pdf)

Murdoch J. Gabbay and Michael Gabbay,

*Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics, February 28-March 1, 2008*.Arbitrary Objects in Mathematics and Semantics
arbomsbibtex
publisherURI
localpdf

Murdoch J. Gabbay and Michael Gabbay,

*Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics, February 28-March 1, 2008*
Towards a Proof-Theoretic Approach to Plurality
(towpta:
bib
URI
pdf)

Michael Gabbay and Murdoch J. Gabbay,

*Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics, February 28-March 1, 2008*.Towards a Proof-Theoretic Approach to Plurality
towptabibtex
publisherURI
localpdf

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

Nominal Algebra
(noma-nwpt:
bib
URI
pdf)

Murdoch J. Gabbay and Aad Mathijssen,

*18th Nordic Workshop on Programming Theory, Reykjavík, Iceland, October 18-20, 2006*.Nominal Algebra
noma-nwptbibtex
publisherURI
localpdf

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. See also Slides of the accompanying talk, and a paper.

Nominal SOS
(nomsos-nwpt:
bib
URI
pdf)

MohammadReza Mousavi, Michel A. Reniers and Murdoch J. Gabbay,

*18th Nordic Workshop on Programming Theory, Reykjavík, Iceland, October 18-20, 2006*.Nominal SOS
nomsos-nwptbibtex
publisherURI
localpdf

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

Nominal Sets, Equivariance Reasoning, and Variable Binding
(nomser:
bib
URI
pdf)

Murdoch J. Gabbay,

*MLG 2002*.Nominal Sets, Equivariance Reasoning, and Variable Binding
nomserbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*MLG 2002* A prose account of my talk at MLG02 in Kinosaki, Japan.

A Theory of Inductive Definitions with Alpha-Equivalence
(thesis:
bib
URI
pdf)

Murdoch J. Gabbay,

*PhD Thesis, Cambridge University, 2001*.A Theory of Inductive Definitions with Alpha-Equivalence
thesisbibtex
publisherURI
localpdf

Murdoch J. Gabbay,

*PhD Thesis, Cambridge University, 2001* See also the survey paper on foundations on nominal techniques.