Papers

SubmittedJournal
InBookConfTechAbstractThesis
 
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
karmbbibtex publisherURI localpdf
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.
JournalSubmittedInBookConfTechAbstractThesis
 
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 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 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
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 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 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.
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.
InBookSubmittedJournalConfTechAbstractThesis
 
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.)
Conference SubmittedJournalInBookTechAbstractThesis
 
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.
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.
Nominal Unification
nomubibtex publisherURI localpdf
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 Urban in Isabelle.
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.
TechReport SubmittedJournalConfInBookAbstractThesis
 
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.
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.
ShortAbstractSubmittedJournalConfInBookTechThesis
 
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
nomserbibtex publisherURI localpdf
Murdoch J. Gabbay, MLG 2002
A prose account of my talk at MLG02 in Kinosaki, Japan.
PhDThesisSubmittedJournalInBookConfTechAbstract
 
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.