Murdoch J. Gabbay

Mathematician, Logician, Academic, Computer scientist, Consultant, Lecturer, Editor

Portrait of Murdoch J. Gabbay
Cathedral photograph

Hello. Thanks for visiting my webpage. I'm a computer science researcher based in Scotland. I got a PhD from Cambridge University in 2001 on the foundations of computation, which introduced "Nominal techniques" <seo>(based on the Gabbay-Pitts model of names in Fraenkel-Mostowski sets)</seo>. This won some prizes.

Nowadays I work on the logic and topological structure of decentralised systems and cryptography; I am very pleased to have applied logic to both. I'm also interested in slide rules, game of life, and other things. I have a wheat intolerance and I do editorial work in academic publishing.

Research

My work connects mathematical logic and theoretical computer science, from the structure of names and binding to models of decentralised action. Click on a topic to jump to papers on that topic.

Publications

I have been fortunate to work with many coauthors, including: Mauricio Ayala-Rincón, Devraj Basu, Lars Brünjes, Ali K. Caires-Santos, James Cheney, Vincenzo Ciancia, Matteo Cimini, Gilles Dowek, Elliot Fairweather, Maribel Fernández, Michael Gabbay, Dan Ghica, Martin Hofmann, Arvid Jakobsson, Peter Kropholler, Stéphane Lengrand, Tadeusz Litak, Ian Mackie, Aad Mathijssen, Orestis Melkonian, Andrew Mendelsohn, Mohammad Reza Mousavi, Dominic Mulligan, Aleksandar Nanevski, Daniele Nantes-Sobrinho, Daniela Petrişan, Andrew Pitts, Michel Reniers, Ana Cristina Rocha-Oliveira, Mark Shinwell, Kristina Sojakova, Christian Urban, Claus-Peter Wirth, and Luca Zanolini.

You can also check me out on DBLP, ORCID, and Scopus.

Selected publications

  1. Publication type: Journal article
  2. Publication type: Journal article
  3. Publication type: Journal article

    Algebras of UTxO blockchains

    Murdoch J. Gabbay

    Mathematical Structures in Computer Science vol. 31, no. 9 In Homage to Martin Hofmann pp. 1034–1089 Cambridge University Press issue dated online

    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.

  4. Publication type: Journal article

    Equivariant ZFA and the foundations of nominal techniques

    Murdoch J. Gabbay

    Journal of Logic and Computation vol. 30, no. 2 pp. 525–548 ISSN 0955-792X online

    A new take on the foundations of nominal techniques.

  5. Publication type: Journal article

    Semantics out of context: nominal absolute denotations for first-order logic and computation

    Murdoch J. Gabbay

    Journal of the ACM vol. 63, no. 3 pp. 1–66 article 25 ISSN 1535-9921

    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.

  6. Publication type: Journal article

    Foundations of nominal techniques: logic and semantics of variables in abstract syntax

    Murdoch J. Gabbay

    Bulletin of Symbolic Logic vol. 17, no. 2 pp. 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.

  7. Publication type: Journal article

    A New Approach to Abstract Syntax with Variable Binding

    Murdoch J. Gabbay, Andrew M. Pitts

    Formal Aspects of Computing vol. 13, no. 3–5 pp. 341–363

    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.

Full publications list

108 items, arranged by date.

Publications by date

2026

  1. Publication type: Conference paper
    Equational Reasoning in Languages with Binders via Permutation Fixed-Points

    Ali K. Caires-Santos, Maribel Fernández, Murdoch James Gabbay, Daniele Nantes-Sobrinho

    11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026) ed. Frank Pfenning Leibniz International Proceedings in Informatics (LIPIcs) vol. 378 pp. 10:1–10:23 article 10 Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik ISBN 978-3-95977-433-8 ISSN 1868-8969

  2. Publication type: Technical report
  3. Publication type: Book chapter
    Decentralized Collaborative Action: Cryptoeconomics in Space

    Murdoch J. Gabbay

    Cryptoeconomic Theory eds. Melanie Swan, Soichiro Takagi, Frank Witte Advances in Science and Technology in the Age of AI vol. 1 pp. 53–70 Singapore: World Scientific ISBN 978-1-80061-865-7 eISBN 978-1-80061-867-1

  4. Publication type: Journal article

2025

  1. Publication type: Preprint
  2. Publication type: Technical report
  3. Publication type: Journal article
  4. Publication type: Journal article
  5. Publication type: Preprint
    A declarative approach to specifying Paxos using three-valued modal fixpoint logic

    Murdoch J. Gabbay, Luca Zanolini

    arXiv latest revision

2024

  1. Publication type: Book
    Semitopology: Decentralised Collaborative Action via Topology, Algebra, and Logic

    Murdoch J. Gabbay

    Studies in Logic vol. 108 320 pp. total London: College Publications edition 1 ISBN 978-1-84890-465-1

2022

  1. Publication type: Journal article
    Algebras of UTxO blockchains

    Murdoch J. Gabbay

    Mathematical Structures in Computer Science vol. 31, no. 9 In Homage to Martin Hofmann pp. 1034–1089 Cambridge University Press issue dated online

    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.

2021

  1. Publication type: Conference paper
    Money Grows on (Proof-)Trees: The Formal FA1.2 Ledger Standard

    Murdoch J. Gabbay, Arvid Jakobsson, Kristina Sojakova

    3rd International Workshop on Formal Methods for Blockchains (FMBC 2021) eds. Bruno Bernardo, Diego Marmsoler Open Access Series in Informatics (OASIcs) vol. 95 pp. 2:1–2:14 article 2 Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik ISBN 978-3-95977-209-9 ISSN 2190-6807

  2. Publication type: Book chapter
    Karl Marx and the Blockchain

    Devraj Basu, Murdoch J. Gabbay

    Media, Technology and Education in a Post-Truth Society ed. Grech, Alex pp. 225–241 Emerald Publishing Limited, Bingley

    We consider blockchain technology from a historical, social, and economic perspective, through a lens of the economic theories of Karl Marx.

2020

  1. Publication type: Conference paper
    UTxO- vs account-based smart contract blockchain programming paradigms

    Lars Brünjes, Murdoch J. Gabbay

    Proceedings of the 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2020) eds. Tiziana Margaria, Bernhard Steffen Lecture Notes in Computer Science vol. 12478 pp. 73–88 Springer

    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.

  2. Publication type: Journal article
    Equivariant ZFA and the foundations of nominal techniques

    Murdoch J. Gabbay

    Journal of Logic and Computation vol. 30, no. 2 pp. 525–548 ISSN 0955-792X online

    A new take on the foundations of nominal techniques.

2018

  1. Publication type: Journal article
    The language of Stratified Sets is confluent and strongly normalising

    Murdoch J. Gabbay

    Logical Methods in Computer Science vol. 14, no. 2 article 12

    Quine’s stratification condition viewed from the perspective of the theory of rewriting.

2017

  1. Publication type: Journal article
    Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness

    Murdoch J. Gabbay, Michael J. Gabbay

    Annals of Pure and Applied Logic vol. 168, no. 3 pp. 501–621 Elsevier

    Everything you wanted to know about semantics of the lambda-calculus using nominal techniques.

2016

  1. Publication type: Journal article
    Checking Overlaps of Nominal Rewriting Rules

    Mauricio Ayala-Rincón, Maribel Fernández, Murdoch James Gabbay, Ana Cristina Rocha-Oliveira

    Electronic Notes in Theoretical Computer Science vol. 323 pp. 39–56 Elsevier B.V. ISSN 1571-0661

  2. Publication type: Journal article
    Semantics out of context: nominal absolute denotations for first-order logic and computation

    Murdoch J. Gabbay

    Journal of the ACM vol. 63, no. 3 pp. 1–66 article 25 ISSN 1535-9921

    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.

2015

  1. Publication type: Conference paper
    Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

    Murdoch J. Gabbay, Dan R. Ghica, Daniela Petrisan

    24th EACSL Annual Conference on Computer Science Logic (CSL 2015) ed. Kreutzer, Stephan Leibniz International Proceedings in Informatics (LIPIcs) vol. 41 pp. 374–389 Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik ISBN 978-3-939897-90-3 ISSN 1868-8969

    Split “νa.t” as “〈a t a〉”. If that looks simple, try “〈a〈b ab a〉b〉” or “〈a〈b abb〉”.

  2. Publication type: Journal article
    Quantifiers in logic and proof-search using permissive-nominal terms and sets

    Murdoch J. Gabbay, Claus-Peter Wirth

    Journal of Logic and Computation vol. 25, no. 2 pp. 473–523

    Nominal terms used to model the γ- and δ-rules controlling quantifiers in reductive proof search.

2014

  1. Publication type: Journal article
  2. Publication type: Book chapter
    Stone duality for First-Order Logic: a nominal approach

    Murdoch J. Gabbay

    HOWARD-60. A Festschrift on the Occasion of Howard Barringer's 60th Birthday eds. Andrei Voronkov, Margarita Korovina EPiC Series in Computing vol. 42 pp. 178–209 EasyChair

    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.

2013

  1. Publication type: Journal article
    Imaginary groups: lazy monoids and reversible computation.

    Murdoch J. Gabbay, Peter Kropholler

    Mathematical Structures in Computer Science vol. 23, no. 05 pp. 1002–1031 Cambridge University Press

    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.

  2. Publication type: Journal article
    Denotation of contextual modal type theory (CMTT): syntax and meta-programming

    Murdoch J. Gabbay, Aleksandar Nanevski

    Journal of Applied Logic vol. 11, no. 1 pp. 1–29

    A denotation for CMTT. I wanted to understand this for years, and now we have an answer!

  3. Publication type: Book chapter
    Nominal terms and nominal logics: from foundations to meta-mathematics

    Murdoch J. Gabbay

    Handbook of Philosophical Logic vol. 17 pp. 79–178 Springer

    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.

2012

  1. Publication type: Journal article
    Meta-variables as infinite lists in nominal terms unification and rewriting

    Murdoch J. Gabbay

    Logic Journal of the IGPL vol. 20, no. 6 pp. 967–1000 Oxford University Press

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

  2. Publication type: Journal article
    Nominal SOS

    Matteo Cimini, Mohammad Reza Mousavi, Michel A. Reniers, Murdoch J. Gabbay

    Electronic Notes in Theoretical Computer Science vol. 286 Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012) pp. 103–116 Elsevier ISSN 1571-0661

  3. Publication type: Journal article
    Game semantics in the nominal model

    Murdoch J. Gabbay, Dan R. Ghica

    Electronic Notes in Theoretical Computer Science vol. 286 Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012) pp. 173–189 Elsevier

    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.

  4. Publication type: Journal article
    PNL to HOL: from the logic of nominal sets to the logic of higher-order functions

    Gilles Dowek, Murdoch J. Gabbay

    Theoretical Computer Science vol. 451 pp. 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.

  5. Publication type: Journal article
    Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free

    Murdoch J. Gabbay

    Journal of Symbolic Logic vol. 77, no. 3 pp. 828–852 Duke University Press

    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.

  6. Publication type: Journal article
    Permissive-nominal logic: First-order logic over nominal terms and sets

    Gilles Dowek, Murdoch J. Gabbay

    ACM Transactions on Computational Logic vol. 13, no. 3 pp. 1–36 article 20 New York: Association for Computing Machinery

    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.

  7. Publication type: Journal article
    Unity in nominal equational reasoning: The algebra of equality on nominal sets

    Murdoch J. Gabbay

    Journal of Applied Logic vol. 10, no. 2 pp. 199–217

    An exhaustive analysis of the design choices involved in nominal equational / equality / algebra logic over nominal sets.

  8. Publication type: Conference paper
    Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits

    Gilles Dowek, Murdoch J. Gabbay

    Proceedings of the 9th Italian Convention on Computational Logic (CILC 2012) ed. Francesca A. Lisi CEUR workshop proceedings vol. 857 pp. 104–118 CEUR-WS.org

    Universal lattice properties used to specify top, meet, and forall as instances of a single notion of fresh-finite limit.

  9. Publication type: Preprint
  10. Publication type: Workshop abstract
    Quantifier rules in reductive proof using nominal semantics

    Murdoch J. Gabbay

    Automated Reasoning Workshop (ARW 2012) 2 pp. total

    We consider liberalised delta-rules in proof-search, and give them a nominal algebraic semantics.

2011

  1. Publication type: Preprint
  2. Publication type: Journal article
    Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables

    Murdoch J. Gabbay

    Mathematical Structures in Computer Science vol. 21, no. 5 pp. 997–1033 Cambridge University Press

    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.

  3. Publication type: Conference paper
    Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets

    Murdoch J. Gabbay, Dominic P. Mulligan

    Proceedings of the 6th International Workshop on Logical Frameworks and Meta-Languages (LFMTP 2011) EPTCS vol. 71 pp. 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.

  4. Publication type: Conference paper
    Principal Types for Nominal Theories

    Elliot Fairweather, Maribel Fernández, Murdoch J. Gabbay

    Proceedings of the 18th International Symposium on Fundamentals of Computation Theory (FCT 2011) eds. Olaf Owe, Martin Steffen, Jan Arne Telle Lecture Notes in Computer Science vol. 6914 pp. 160–172 Berlin, Heidelberg: Springer ISBN 978-3-642-22952-7 eISBN 978-3-642-22953-4

    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.

  5. Publication type: Conference paper
    Stone duality for nominal Boolean algebras with NEW

    Murdoch J. Gabbay, Tadeusz Litak, Daniela Petrişan

    Proceedings of the 4th international conference on algebra and coalgebra in computer science (CALCO 2011) Lecture Notes in Computer Science vol. 6859 pp. 192–207 Springer ISBN 978-3-642-22943-5

    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.

  6. Publication type: Journal article
    Foundations of nominal techniques: logic and semantics of variables in abstract syntax

    Murdoch J. Gabbay

    Bulletin of Symbolic Logic vol. 17, no. 2 pp. 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.

  7. Publication type: Conference paper
    Freshness and name-restriction in sets of traces with names

    Murdoch J. Gabbay, Vincenzo Ciancia

    Foundations of software science and computation structures, 14th International Conference (FOSSACS 2011) Lecture Notes in Computer Science vol. 6604 pp. 365–380 Springer

    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.

  8. Publication type: Workshop abstract
    Metamathematics based on nominal terms and nominal logic: foundations of a nominal theorem-prover

    Murdoch J. Gabbay

    Automated Reasoning Workshop (ARW 2011) 2 pp. total

    We sketch what theorem-proving might look like if it were based on nominal terms. This eventually evolved into Nominal terms and nominal logics.

2010

  1. Publication type: Conference paper
    A simple class of Kripke-style models in which logic and computation have equal standing

    Michael J. Gabbay, Murdoch J. Gabbay

    International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2010) eds. Edmund M. Clarke, Andrei Voronkov Lecture Notes in Computer Science vol. 6355 pp. 231–254 Springer

    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.

  2. Publication type: Journal article
    Permissive Nominal Terms and their Unification: an infinite, co-infinite approach to nominal techniques (journal version)

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

    Logic Journal of the IGPL vol. 18, no. 6 pp. 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.

  3. Publication type: Conference paper
    Closed nominal rewriting and efficiently computable nominal algebra equality

    Maribel Fernández, Murdoch J. Gabbay

    Electronic Proceedings in Theoretical Computer Science vol. 34 pp. 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.

  4. Publication type: Conference paper
    Permissive Nominal Logic

    Gilles Dowek, Murdoch J. Gabbay

    Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2010) pp. 165–176 New York: ACM Press

    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.

  5. Publication type: Technical report
    An observation on support and freshness in nominal sets

    Murdoch J. Gabbay

    School of Mathematical and Computer Sciences, Heriot-Watt University Technical Report no. HW-MACS-TR-0077 14 pp. total Edinburgh, UK

    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.

  6. Publication type: Journal article
    A nominal axiomatisation of the lambda-calculus

    Murdoch J. Gabbay, Aad Mathijssen

    Journal of Logic and Computation vol. 20, no. 2 pp. 501–531

    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.

  7. Publication type: Journal article
    Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

    Murdoch J. Gabbay, Dominic P. Mulligan

    Information and Computation vol. 208, no. 3 pp. 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.

2009

  1. Publication type: Journal article
    Nominal universal algebra: equational logic with names and binding

    Murdoch J. Gabbay, Aad Mathijssen

    Journal of Logic and Computation vol. 19, no. 6 pp. 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

  2. Publication type: Journal article
    The lambda-context calculus (extended version)

    Murdoch J. Gabbay, Stéphane Lengrand

    Information and computation vol. 207, no. 12 pp. 1369–1400 Elsevier

    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.

  3. Publication type: Conference paper
    Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables

    Murdoch J. Gabbay, Dominic P. Mulligan

    Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFMTP 2009) pp. 64–73 ACM

    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.

  4. Publication type: Conference paper
    Two-level lambda-calculus

    Murdoch J. Gabbay, Dominic P. Mulligan

    Electronic Notes in Theoretical Computer Science vol. 246 pp. 107–129

    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.

  5. Publication type: Conference paper
    Term sequent logic

    Michael Gabbay, Murdoch J. Gabbay

    Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008) Electronic Notes in Theoretical Computer Science vol. 246 pp. 87–106

    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.

  6. Publication type: Conference paper
    Permissive Nominal Terms and their Unification

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

    Atti del Convegno CILC 09: 24-esimo Convegno Italiano di Logica Computazionale eds. Marco Gavanelli, Fabrizio Riguzzi pp. 70–84 Ferrara, Italy: GULP (Italian Association for Logic Programming)

    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

  7. Publication type: Journal article
    Nominal Algebra and the HSP Theorem

    Murdoch J. Gabbay

    Journal of Logic and Computation vol. 19, no. 2 pp. 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.

  8. Publication type: Conference paper
    Semantic nominal terms

    Murdoch J. Gabbay, Dominic P. Mulligan

    Second International Workshop on Theory and Applications of Abstraction, Substitution, and Naming (TAASN 2009), associated with ETAPS 2009 5 pp. total York, UK

    We reconcile nominal atoms-abstraction with nominal terms. See the journal paper on two-level nominal sets.

  9. Publication type: Journal article
    A study of substitution, using nominal techniques and Fraenkel-Mostowski sets

    Murdoch J. Gabbay

    Theoretical Computer Science vol. 410, no. 12-13 pp. 1159–1189 Elsevier

    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.

  10. Publication type: Technical report
    Permissive Nominal Terms and their Unification

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

    School of Mathematical and Computer Sciences, Heriot-Watt University Technical Report no. HW-MACS-TR-0062 49 pp. total Edinburgh, UK

    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.

2008

  1. Publication type: Book chapter
    The lambda-calculus is nominal algebraic

    Murdoch J. Gabbay, Aad Mathijssen

    Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on his 70th Birthday eds. Christoph Benzmüller, Chad E. Brown, Jörg Siekmann, Richard Statman Studies in Logic vol. 17 pp. 271–302 London: College Publications 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.

  2. Publication type: Conference paper
    Nominal renaming sets

    Murdoch J. Gabbay, Martin Hofmann

    Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008) pp. 158–173 Springer

    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.

  3. Publication type: Technical report
    Permissive nominal terms

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

    INRIA Research Report no. RR-6682 15 pp. total Orsay, France

    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.

  4. Publication type: Journal article
    One-and-a-halfth-order Logic

    Murdoch J. Gabbay, Aad Mathijssen

    Journal of Logic and Computation vol. 18, no. 4 pp. 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.

  5. Publication type: Journal article
    a-logic with arrows (journal version)

    Murdoch J. Gabbay, Michael J. Gabbay

    Electronic Notes in Theoretical Computer Science vol. 216 pp. 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.

  6. Publication type: Conference paper
    One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations

    Murdoch J. Gabbay, Dominic P. Mulligan

    Proceedings of 15th Workshop on Logic, Language and Information in Computation (WoLLIC 2008) Lecture Notes in Artificial Intelligence vol. 5110 pp. 179–193 Springer

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

  7. Publication type: Journal article
    Capture-Avoiding Substitution as a Nominal Algebra

    Murdoch J. Gabbay, Aad Mathijssen

    Formal Aspects of Computing vol. 20, no. 4-5 pp. 451–479 Springer

    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.

  8. Publication type: Conference paper
    Substitution for Fraenkel-Mostowski foundations

    Murdoch J. Gabbay, Michael J. Gabbay

    Proceedings of the 2008 AISB Symposium on Computing and Philosophy AISB 2008 Convention: Communication, Interaction and Social Intelligence vol. 12 pp. 65–72 University of Aberdeen, Aberdeen, UK: The Society for the Study of Artificial Intelligence and Simulation of Behaviour ISBN 1-902956-71-0

    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.

  9. Publication type: Workshop abstract
    Towards a Proof-Theoretic Approach to Plurality: Numbers Are Logical Constants

    Michael J. Gabbay, Murdoch J. Gabbay

    Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics 2 pp. total Paris, France

  10. Publication type: Workshop abstract
    Arbitrary Objects in Mathematics and Semantics

    Murdoch J. Gabbay, Michael J. Gabbay

    Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics 2 pp. total Paris, France

    A photo of Michael delivering the talk.

  11. Publication type: Journal article
    The lambda-context calculus

    Murdoch J. Gabbay, Stéphane Lengrand

    Electronic Notes in Theoretical Computer Science vol. 196 pp. 19–35 Elsevier ISSN 1571-0661

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

2007

  1. Publication type: Technical report
    Nominal renaming sets

    Murdoch J. Gabbay

    Heriot-Watt University Technical Report no. HW-MACS-TR-0058 35 pp. total Edinburgh, UK

    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.

  2. Publication type: Technical report
    Nominal Algebra and the HSP Theorem

    Murdoch J. Gabbay, Aad Mathijssen

    Heriot-Watt University HW-MACS-TR-0057

    Subsumed by “Nominal Algebra and the HSP Theorem”.

    We prove the HSP (Homomorphism, Subalgebra, Product) theorem for Nominal Algebra, also known as Birkhoffs theorem.

  3. Publication type: Book chapter
    Curry-style types for nominal terms

    Maribel Fernández, Murdoch J. Gabbay

    Types for Proofs and Programs (TYPES 06) Lecture Notes in Computer Science vol. 4502 pp. 125–139 Springer

    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.

  4. Publication type: Conference paper
    A Formal Calculus for Informal Equality with Binding

    Murdoch J. Gabbay, Aad Mathijssen

    WoLLIC'07: 14th Workshop on Logic, Language, Information and Computation Lecture Notes in Computer Science vol. 4576 pp. 162–176 Springer

    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.

  5. Publication type: Journal article
    A General Mathematics of Names

    Murdoch J. Gabbay

    Information and Computation vol. 205, no. 7 pp. 982–1011 Academic Press

    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.

  6. Publication type: Conference paper
    a-logic with arrows

    Murdoch J. Gabbay, Michael J. Gabbay

    Proceedings of the 16th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2007), held at RDP 2007 pp. 47–62 Paris, France

    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.

  7. Publication type: Journal article
    Nominal rewriting (journal version)

    Maribel Fernández, Murdoch J. Gabbay

    Information and Computation vol. 205, no. 6 pp. 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.

  8. Publication type: Journal article
    Hierarchical Nominal Terms and Their Theory of Rewriting

    Murdoch J. Gabbay

    Electronic Notes in Theoretical Computer Science vol. 174, no. 5 pp. 37–52 Elsevier ISSN 1571-0661

    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.

  9. Publication type: Journal article
    Fresh Logic: proof-theory and semantics for FM and nominal techniques

    Murdoch J. Gabbay

    Journal of Applied Logic vol. 5, no. 2 pp. 356–387 Elsevier

    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.

  10. Publication type: Technical report
    Capture-Avoiding Substitution as a Nominal Algebra

    Murdoch J. Gabbay, Aad Mathijssen

    Heriot-Watt University HW-MACS-TR-0053

    Subsumed by “Capture-Avoiding Substitution as a Nominal Algebra”.

    Decidability and theory of models of a nominal algebra axiomatisation of capture-avoiding substitution.

2006

  1. Publication type: Conference paper
    Capture-avoiding Substitution as a Nominal Algebra

    Murdoch J. Gabbay, Aad Mathijssen

    Proceedings of the 3rd International Colloquium on Theoretical Aspects of Computing (ICTAC 2006) Lecture Notes in Computer Science vol. 4281 pp. 198–212 Berlin: Springer

    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.

  2. Publication type: Workshop abstract
    Nominal SOS

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

    Proceedings of the 18th Nordic Workshop on Programming Theory (NWPT'06) 2 pp. total Reykjavík, Iceland

    We describe Nominal Structured Operational Semantics, a framework for specifying operational semantics within which proofs of congruence are carried out ‘once and for all’.

  3. Publication type: Workshop abstract
    Nominal Algebra

    Murdoch J. Gabbay, Aad Mathijssen

    Proceedings of the 18th Nordic Workshop on Programming Theory (NWPT'06) 3 pp. total Reykjavík, Iceland

    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.

  4. Publication type: Conference paper
  5. Publication type: Conference paper
    One-and-a-halfth-order logic

    Murdoch J. Gabbay, Aad Mathijssen

    Proceedings of the 8th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2006) pp. 189–200 ACM ISBN 1-59593-388-3

    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.

2005

  1. Publication type: Book chapter
    Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning

    Michael J. Gabbay, Murdoch J. Gabbay

    We Will Show Them: Essays in Honour of Dov Gabbay eds. S. Artemov, H. Barringer, A. d'Avila Garcez, Luis C. Lamb, J. Woods vol. 1 pp. 701–730 London: College Publications ISBN 1-904987-11-7 (pb); 1-904987-25-7 (hb)

    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.

  2. Publication type: Book chapter
    a-logic

    Murdoch J. Gabbay, Michael J. Gabbay

    We Will Show Them: Essays in Honour of Dov Gabbay eds. S. Artemov, H. Barringer, A. d'Avila Garcez, Luis C. Lamb, J. Woods vol. 1 pp. 731–764 London: College Publications ISBN 1-904987-11-7 (pb); 1-904987-25-7 (hb)

    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.

  3. Publication type: Conference paper
    SOS for Higher Order Processes (Extended Abstract)

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

    Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05) eds. Abadi, Martin; de Alfaro, Luca Lecture Notes in Computer Science vol. 3653 pp. 308–322 Springer

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

  4. Publication type: Conference paper
    A NEW calculus of contexts

    Murdoch J. Gabbay

    Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP '05) eds. Pedro Barahona, Amy P. Felty pp. 94–105 Lisbon, Portugal: Association for Computing Machinery ISBN 1-59593-090-6

    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.

  5. Publication type: Conference paper

2004

  1. Publication type: Journal article
    Nominal Unification

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

    Theoretical Computer Science vol. 323, no. 1–3 pp. 473–497 Essex, UK: Elsevier ISSN 0304-3975

    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.

  2. Publication type: Conference paper
    Nominal Rewriting Systems

    Maribel Fernández, Murdoch J. Gabbay, Ian Mackie

    Proceedings of the 6th ACM SIGPLAN symposium on Principles and Practice of Declarative Programming (PPDP 2004) pp. 108–119 ACM Press

    We generalise first-order rewriting with terms involving binding operations, using a nominal approach in which bound entities are explicitly named.

  3. Publication type: Conference paper
    A Sequent Calculus for Nominal Logic

    Murdoch J. Gabbay, James Cheney

    Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004) pp. 139–148 IEEE Computer Society

    A sequent calculus for Nominal Logic. We consider notions of Logic Programming in it and give a translation of Miller and Tiu’s FOLN.

2003

  1. Publication type: Conference paper
    Nominal Unification

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

    Proceedings of the 17th International Workshop on Computer Science Logic (CSL 2003) Lecture Notes in Computer Science vol. 2803 pp. 513–527 Springer

    See here for formal verification of the results Urban in Isabelle.

  2. Publication type: Book chapter
    The π-Calculus in FM

    Murdoch J. Gabbay

    Thirty-five years of Automating Mathematics ed. Fairouz D. Kamareddine Applied Logic Series vol. 28 pp. 247–269 Dordrecht: Kluwer Academic Publishers edition 1 ISBN 978-1-4020-1656-1 eISBN 978-94-017-0253-9

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

  3. Publication type: Conference paper
    FreshML: Programming with Binders Made Simple

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

    SIGPLAN Notices vol. 38 pp. 263–274 ACM Press

    ML enriched with Gabbay-Pitts atoms-abstraction and nominal name-generation and pattern-matching.

2002

  1. Publication type: Conference paper
    Automating Fraenkel-Mostowski Syntax

    Murdoch J. Gabbay

    Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002) eds. Víctor A. Carreño, César A. Muñoz, Sofiène Tahar NASA Conference Publication vol. NASA/CP-2002-211736 pp. 60–70 Hampton, Virginia, USA: National Aeronautics and Space Administration, Langley Research Center

  2. Publication type: Journal article
    A New Approach to Abstract Syntax with Variable Binding

    Murdoch J. Gabbay, Andrew M. Pitts

    Formal Aspects of Computing vol. 13, no. 3–5 pp. 341–363

    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.

  3. Publication type: Conference paper
    FM-HOL, a higher-order theory of names

    Murdoch J. Gabbay

    Informal Proceedings of the Workshop on Thirty Five Years of Automath ed. Fairouz Kamareddine Edinburgh, Scotland: Heriot-Watt University

    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.

  4. Publication type: Workshop abstract
    Nominal Sets, Equivariance Reasoning, and Variable Binding

    Murdoch J. Gabbay

    Second Workshop on Meta-Logic (MLG 2002) 2 pp. total Kinosaki, Japan

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

2001

  1. Publication type: Doctoral thesis
    A Theory of Inductive Definitions with α-Equivalence: Semantics, Implementation, Programming Language

    Murdoch J. Gabbay

    University of Cambridge Cambridge, UK

    See also the survey paper on foundations on nominal techniques.

2000

  1. Publication type: Conference paper

1999

  1. Publication type: Conference paper

Publications by topic

Some publications appear under more than one topic.

Cryptography 1 publication
  1. Publication type: Journal article
Decentralised systems 12 publications
  1. Publication type: Technical report
  2. Publication type: Book chapter
    Decentralized Collaborative Action: Cryptoeconomics in Space

    Murdoch J. Gabbay

    Cryptoeconomic Theory eds. Melanie Swan, Soichiro Takagi, Frank Witte Advances in Science and Technology in the Age of AI vol. 1 pp. 53–70 Singapore: World Scientific ISBN 978-1-80061-865-7 eISBN 978-1-80061-867-1

  3. Publication type: Journal article
  4. Publication type: Preprint
  5. Publication type: Technical report
  6. Publication type: Journal article
  7. Publication type: Preprint
    A declarative approach to specifying Paxos using three-valued modal fixpoint logic

    Murdoch J. Gabbay, Luca Zanolini

    arXiv latest revision

  8. Publication type: Book
    Semitopology: Decentralised Collaborative Action via Topology, Algebra, and Logic

    Murdoch J. Gabbay

    Studies in Logic vol. 108 320 pp. total London: College Publications edition 1 ISBN 978-1-84890-465-1

  9. Publication type: Journal article
    Algebras of UTxO blockchains

    Murdoch J. Gabbay

    Mathematical Structures in Computer Science vol. 31, no. 9 In Homage to Martin Hofmann pp. 1034–1089 Cambridge University Press issue dated online

    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.

  10. Publication type: Conference paper
    Money Grows on (Proof-)Trees: The Formal FA1.2 Ledger Standard

    Murdoch J. Gabbay, Arvid Jakobsson, Kristina Sojakova

    3rd International Workshop on Formal Methods for Blockchains (FMBC 2021) eds. Bruno Bernardo, Diego Marmsoler Open Access Series in Informatics (OASIcs) vol. 95 pp. 2:1–2:14 article 2 Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik ISBN 978-3-95977-209-9 ISSN 2190-6807

  11. Publication type: Book chapter
    Karl Marx and the Blockchain

    Devraj Basu, Murdoch J. Gabbay

    Media, Technology and Education in a Post-Truth Society ed. Grech, Alex pp. 225–241 Emerald Publishing Limited, Bingley

    We consider blockchain technology from a historical, social, and economic perspective, through a lens of the economic theories of Karl Marx.

  12. Publication type: Conference paper
    UTxO- vs account-based smart contract blockchain programming paradigms

    Lars Brünjes, Murdoch J. Gabbay

    Proceedings of the 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2020) eds. Tiziana Margaria, Bernhard Steffen Lecture Notes in Computer Science vol. 12478 pp. 73–88 Springer

    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.

Declarative distributed protocols 4 publications
  1. Publication type: Technical report
  2. Publication type: Preprint
  3. Publication type: Technical report
  4. Publication type: Preprint
    A declarative approach to specifying Paxos using three-valued modal fixpoint logic

    Murdoch J. Gabbay, Luca Zanolini

    arXiv latest revision

Lambda calculus and metaprogramming 15 publications
  1. Publication type: Journal article
    Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness

    Murdoch J. Gabbay, Michael J. Gabbay

    Annals of Pure and Applied Logic vol. 168, no. 3 pp. 501–621 Elsevier

    Everything you wanted to know about semantics of the lambda-calculus using nominal techniques.

  2. Publication type: Journal article
  3. Publication type: Journal article
    Denotation of contextual modal type theory (CMTT): syntax and meta-programming

    Murdoch J. Gabbay, Aleksandar Nanevski

    Journal of Applied Logic vol. 11, no. 1 pp. 1–29

    A denotation for CMTT. I wanted to understand this for years, and now we have an answer!

  4. Publication type: Preprint
  5. Publication type: Conference paper
    Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets

    Murdoch J. Gabbay, Dominic P. Mulligan

    Proceedings of the 6th International Workshop on Logical Frameworks and Meta-Languages (LFMTP 2011) EPTCS vol. 71 pp. 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.

  6. Publication type: Conference paper
    A simple class of Kripke-style models in which logic and computation have equal standing

    Michael J. Gabbay, Murdoch J. Gabbay

    International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2010) eds. Edmund M. Clarke, Andrei Voronkov Lecture Notes in Computer Science vol. 6355 pp. 231–254 Springer

    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.

  7. Publication type: Journal article
    A nominal axiomatisation of the lambda-calculus

    Murdoch J. Gabbay, Aad Mathijssen

    Journal of Logic and Computation vol. 20, no. 2 pp. 501–531

    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.

  8. Publication type: Journal article
    Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

    Murdoch J. Gabbay, Dominic P. Mulligan

    Information and Computation vol. 208, no. 3 pp. 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.

  9. Publication type: Journal article
    The lambda-context calculus (extended version)

    Murdoch J. Gabbay, Stéphane Lengrand

    Information and computation vol. 207, no. 12 pp. 1369–1400 Elsevier

    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.

  10. Publication type: Conference paper
    Two-level lambda-calculus

    Murdoch J. Gabbay, Dominic P. Mulligan

    Electronic Notes in Theoretical Computer Science vol. 246 pp. 107–129

    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.

  11. Publication type: Conference paper
    Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables

    Murdoch J. Gabbay, Dominic P. Mulligan

    Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFMTP 2009) pp. 64–73 ACM

    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.

  12. Publication type: Book chapter
    The lambda-calculus is nominal algebraic

    Murdoch J. Gabbay, Aad Mathijssen

    Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on his 70th Birthday eds. Christoph Benzmüller, Chad E. Brown, Jörg Siekmann, Richard Statman Studies in Logic vol. 17 pp. 271–302 London: College Publications 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.

  13. Publication type: Conference paper
    One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations

    Murdoch J. Gabbay, Dominic P. Mulligan

    Proceedings of 15th Workshop on Logic, Language and Information in Computation (WoLLIC 2008) Lecture Notes in Artificial Intelligence vol. 5110 pp. 179–193 Springer

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

  14. Publication type: Journal article
    The lambda-context calculus

    Murdoch J. Gabbay, Stéphane Lengrand

    Electronic Notes in Theoretical Computer Science vol. 196 pp. 19–35 Elsevier ISSN 1571-0661

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

  15. Publication type: Conference paper
    A NEW calculus of contexts

    Murdoch J. Gabbay

    Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP '05) eds. Pedro Barahona, Amy P. Felty pp. 94–105 Lisbon, Portugal: Association for Computing Machinery ISBN 1-59593-090-6

    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.

Logic and proof theory 33 publications
  1. Publication type: Preprint
  2. Publication type: Journal article
  3. Publication type: Preprint
    A declarative approach to specifying Paxos using three-valued modal fixpoint logic

    Murdoch J. Gabbay, Luca Zanolini

    arXiv latest revision

  4. Publication type: Journal article
    Quantifiers in logic and proof-search using permissive-nominal terms and sets

    Murdoch J. Gabbay, Claus-Peter Wirth

    Journal of Logic and Computation vol. 25, no. 2 pp. 473–523

    Nominal terms used to model the γ- and δ-rules controlling quantifiers in reductive proof search.

  5. Publication type: Book chapter
    Nominal terms and nominal logics: from foundations to meta-mathematics

    Murdoch J. Gabbay

    Handbook of Philosophical Logic vol. 17 pp. 79–178 Springer

    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.

  6. Publication type: Journal article
    PNL to HOL: from the logic of nominal sets to the logic of higher-order functions

    Gilles Dowek, Murdoch J. Gabbay

    Theoretical Computer Science vol. 451 pp. 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.

  7. Publication type: Journal article
    Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free

    Murdoch J. Gabbay

    Journal of Symbolic Logic vol. 77, no. 3 pp. 828–852 Duke University Press

    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.

  8. Publication type: Journal article
    Permissive-nominal logic: First-order logic over nominal terms and sets

    Gilles Dowek, Murdoch J. Gabbay

    ACM Transactions on Computational Logic vol. 13, no. 3 pp. 1–36 article 20 New York: Association for Computing Machinery

    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.

  9. Publication type: Journal article
    Unity in nominal equational reasoning: The algebra of equality on nominal sets

    Murdoch J. Gabbay

    Journal of Applied Logic vol. 10, no. 2 pp. 199–217

    An exhaustive analysis of the design choices involved in nominal equational / equality / algebra logic over nominal sets.

  10. Publication type: Workshop abstract
    Quantifier rules in reductive proof using nominal semantics

    Murdoch J. Gabbay

    Automated Reasoning Workshop (ARW 2012) 2 pp. total

    We consider liberalised delta-rules in proof-search, and give them a nominal algebraic semantics.

  11. Publication type: Preprint
  12. Publication type: Workshop abstract
    Metamathematics based on nominal terms and nominal logic: foundations of a nominal theorem-prover

    Murdoch J. Gabbay

    Automated Reasoning Workshop (ARW 2011) 2 pp. total

    We sketch what theorem-proving might look like if it were based on nominal terms. This eventually evolved into Nominal terms and nominal logics.

  13. Publication type: Conference paper
    A simple class of Kripke-style models in which logic and computation have equal standing

    Michael J. Gabbay, Murdoch J. Gabbay

    International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2010) eds. Edmund M. Clarke, Andrei Voronkov Lecture Notes in Computer Science vol. 6355 pp. 231–254 Springer

    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.

  14. Publication type: Conference paper
    Permissive Nominal Logic

    Gilles Dowek, Murdoch J. Gabbay

    Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2010) pp. 165–176 New York: ACM Press

    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.

  15. Publication type: Journal article
    Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

    Murdoch J. Gabbay, Dominic P. Mulligan

    Information and Computation vol. 208, no. 3 pp. 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.

  16. Publication type: Journal article
    Nominal universal algebra: equational logic with names and binding

    Murdoch J. Gabbay, Aad Mathijssen

    Journal of Logic and Computation vol. 19, no. 6 pp. 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

  17. Publication type: Conference paper
    Term sequent logic

    Michael Gabbay, Murdoch J. Gabbay

    Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008) Electronic Notes in Theoretical Computer Science vol. 246 pp. 87–106

    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.

  18. Publication type: Journal article
    Nominal Algebra and the HSP Theorem

    Murdoch J. Gabbay

    Journal of Logic and Computation vol. 19, no. 2 pp. 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.

  19. Publication type: Journal article
    One-and-a-halfth-order Logic

    Murdoch J. Gabbay, Aad Mathijssen

    Journal of Logic and Computation vol. 18, no. 4 pp. 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.

  20. Publication type: Journal article
    a-logic with arrows (journal version)

    Murdoch J. Gabbay, Michael J. Gabbay

    Electronic Notes in Theoretical Computer Science vol. 216 pp. 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.

  21. Publication type: Conference paper
    One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations

    Murdoch J. Gabbay, Dominic P. Mulligan

    Proceedings of 15th Workshop on Logic, Language and Information in Computation (WoLLIC 2008) Lecture Notes in Artificial Intelligence vol. 5110 pp. 179–193 Springer

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

  22. Publication type: Workshop abstract
    Towards a Proof-Theoretic Approach to Plurality: Numbers Are Logical Constants

    Michael J. Gabbay, Murdoch J. Gabbay

    Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics 2 pp. total Paris, France

  23. Publication type: Technical report
    Nominal Algebra and the HSP Theorem

    Murdoch J. Gabbay, Aad Mathijssen

    Heriot-Watt University HW-MACS-TR-0057

    Subsumed by “Nominal Algebra and the HSP Theorem”.

    We prove the HSP (Homomorphism, Subalgebra, Product) theorem for Nominal Algebra, also known as Birkhoffs theorem.

  24. Publication type: Conference paper
    A Formal Calculus for Informal Equality with Binding

    Murdoch J. Gabbay, Aad Mathijssen

    WoLLIC'07: 14th Workshop on Logic, Language, Information and Computation Lecture Notes in Computer Science vol. 4576 pp. 162–176 Springer

    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.

  25. Publication type: Conference paper
    a-logic with arrows

    Murdoch J. Gabbay, Michael J. Gabbay

    Proceedings of the 16th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2007), held at RDP 2007 pp. 47–62 Paris, France

    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.

  26. Publication type: Journal article
    Fresh Logic: proof-theory and semantics for FM and nominal techniques

    Murdoch J. Gabbay

    Journal of Applied Logic vol. 5, no. 2 pp. 356–387 Elsevier

    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.

  27. Publication type: Workshop abstract
    Nominal Algebra

    Murdoch J. Gabbay, Aad Mathijssen

    Proceedings of the 18th Nordic Workshop on Programming Theory (NWPT'06) 3 pp. total Reykjavík, Iceland

    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.

  28. Publication type: Conference paper
    One-and-a-halfth-order logic

    Murdoch J. Gabbay, Aad Mathijssen

    Proceedings of the 8th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2006) pp. 189–200 ACM ISBN 1-59593-388-3

    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.

  29. Publication type: Book chapter
    Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning

    Michael J. Gabbay, Murdoch J. Gabbay

    We Will Show Them: Essays in Honour of Dov Gabbay eds. S. Artemov, H. Barringer, A. d'Avila Garcez, Luis C. Lamb, J. Woods vol. 1 pp. 701–730 London: College Publications ISBN 1-904987-11-7 (pb); 1-904987-25-7 (hb)

    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.

  30. Publication type: Book chapter
    a-logic

    Murdoch J. Gabbay, Michael J. Gabbay

    We Will Show Them: Essays in Honour of Dov Gabbay eds. S. Artemov, H. Barringer, A. d'Avila Garcez, Luis C. Lamb, J. Woods vol. 1 pp. 731–764 London: College Publications ISBN 1-904987-11-7 (pb); 1-904987-25-7 (hb)

    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.

  31. Publication type: Conference paper
    A Sequent Calculus for Nominal Logic

    Murdoch J. Gabbay, James Cheney

    Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004) pp. 139–148 IEEE Computer Society

    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 sets and foundations 23 publications
  1. Publication type: Journal article
    Equivariant ZFA and the foundations of nominal techniques

    Murdoch J. Gabbay

    Journal of Logic and Computation vol. 30, no. 2 pp. 525–548 ISSN 0955-792X online

    A new take on the foundations of nominal techniques.

  2. Publication type: Journal article
    The language of Stratified Sets is confluent and strongly normalising

    Murdoch J. Gabbay

    Logical Methods in Computer Science vol. 14, no. 2 article 12

    Quine’s stratification condition viewed from the perspective of the theory of rewriting.

  3. Publication type: Conference paper
    Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

    Murdoch J. Gabbay, Dan R. Ghica, Daniela Petrisan

    24th EACSL Annual Conference on Computer Science Logic (CSL 2015) ed. Kreutzer, Stephan Leibniz International Proceedings in Informatics (LIPIcs) vol. 41 pp. 374–389 Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik ISBN 978-3-939897-90-3 ISSN 1868-8969

    Split “νa.t” as “〈a t a〉”. If that looks simple, try “〈a〈b ab a〉b〉” or “〈a〈b abb〉”.

  4. Publication type: Book chapter
    Nominal terms and nominal logics: from foundations to meta-mathematics

    Murdoch J. Gabbay

    Handbook of Philosophical Logic vol. 17 pp. 79–178 Springer

    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.

  5. Publication type: Journal article
    Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables

    Murdoch J. Gabbay

    Mathematical Structures in Computer Science vol. 21, no. 5 pp. 997–1033 Cambridge University Press

    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.

  6. Publication type: Journal article
    Foundations of nominal techniques: logic and semantics of variables in abstract syntax

    Murdoch J. Gabbay

    Bulletin of Symbolic Logic vol. 17, no. 2 pp. 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.

  7. Publication type: Conference paper
    Freshness and name-restriction in sets of traces with names

    Murdoch J. Gabbay, Vincenzo Ciancia

    Foundations of software science and computation structures, 14th International Conference (FOSSACS 2011) Lecture Notes in Computer Science vol. 6604 pp. 365–380 Springer

    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.

  8. Publication type: Technical report
    An observation on support and freshness in nominal sets

    Murdoch J. Gabbay

    School of Mathematical and Computer Sciences, Heriot-Watt University Technical Report no. HW-MACS-TR-0077 14 pp. total Edinburgh, UK

    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.

  9. Publication type: Conference paper
    Semantic nominal terms

    Murdoch J. Gabbay, Dominic P. Mulligan

    Second International Workshop on Theory and Applications of Abstraction, Substitution, and Naming (TAASN 2009), associated with ETAPS 2009 5 pp. total York, UK

    We reconcile nominal atoms-abstraction with nominal terms. See the journal paper on two-level nominal sets.

  10. Publication type: Conference paper
    Nominal renaming sets

    Murdoch J. Gabbay, Martin Hofmann

    Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008) pp. 158–173 Springer

    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.

  11. Publication type: Workshop abstract
    Arbitrary Objects in Mathematics and Semantics

    Murdoch J. Gabbay, Michael J. Gabbay

    Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics 2 pp. total Paris, France

    A photo of Michael delivering the talk.

  12. Publication type: Technical report
    Nominal renaming sets

    Murdoch J. Gabbay

    Heriot-Watt University Technical Report no. HW-MACS-TR-0058 35 pp. total Edinburgh, UK

    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.

  13. Publication type: Book chapter
    Curry-style types for nominal terms

    Maribel Fernández, Murdoch J. Gabbay

    Types for Proofs and Programs (TYPES 06) Lecture Notes in Computer Science vol. 4502 pp. 125–139 Springer

    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.

  14. Publication type: Journal article
    A General Mathematics of Names

    Murdoch J. Gabbay

    Information and Computation vol. 205, no. 7 pp. 982–1011 Academic Press

    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.

  15. Publication type: Book chapter
    Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning

    Michael J. Gabbay, Murdoch J. Gabbay

    We Will Show Them: Essays in Honour of Dov Gabbay eds. S. Artemov, H. Barringer, A. d'Avila Garcez, Luis C. Lamb, J. Woods vol. 1 pp. 701–730 London: College Publications ISBN 1-904987-11-7 (pb); 1-904987-25-7 (hb)

    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.

  16. Publication type: Conference paper
    A NEW calculus of contexts

    Murdoch J. Gabbay

    Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP '05) eds. Pedro Barahona, Amy P. Felty pp. 94–105 Lisbon, Portugal: Association for Computing Machinery ISBN 1-59593-090-6

    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.

  17. Publication type: Conference paper
    Automating Fraenkel-Mostowski Syntax

    Murdoch J. Gabbay

    Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002) eds. Víctor A. Carreño, César A. Muñoz, Sofiène Tahar NASA Conference Publication vol. NASA/CP-2002-211736 pp. 60–70 Hampton, Virginia, USA: National Aeronautics and Space Administration, Langley Research Center

  18. Publication type: Journal article
    A New Approach to Abstract Syntax with Variable Binding

    Murdoch J. Gabbay, Andrew M. Pitts

    Formal Aspects of Computing vol. 13, no. 3–5 pp. 341–363

    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.

  19. Publication type: Conference paper
    FM-HOL, a higher-order theory of names

    Murdoch J. Gabbay

    Informal Proceedings of the Workshop on Thirty Five Years of Automath ed. Fairouz Kamareddine Edinburgh, Scotland: Heriot-Watt University

    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.

  20. Publication type: Workshop abstract
    Nominal Sets, Equivariance Reasoning, and Variable Binding

    Murdoch J. Gabbay

    Second Workshop on Meta-Logic (MLG 2002) 2 pp. total Kinosaki, Japan

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

  21. Publication type: Doctoral thesis
    A Theory of Inductive Definitions with α-Equivalence: Semantics, Implementation, Programming Language

    Murdoch J. Gabbay

    University of Cambridge Cambridge, UK

    See also the survey paper on foundations on nominal techniques.

  22. Publication type: Conference paper
Programming languages and processes 8 publications
  1. Publication type: Conference paper
    UTxO- vs account-based smart contract blockchain programming paradigms

    Lars Brünjes, Murdoch J. Gabbay

    Proceedings of the 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2020) eds. Tiziana Margaria, Bernhard Steffen Lecture Notes in Computer Science vol. 12478 pp. 73–88 Springer

    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.

  2. Publication type: Journal article
    Nominal SOS

    Matteo Cimini, Mohammad Reza Mousavi, Michel A. Reniers, Murdoch J. Gabbay

    Electronic Notes in Theoretical Computer Science vol. 286 Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012) pp. 103–116 Elsevier ISSN 1571-0661

  3. Publication type: Workshop abstract
    Nominal SOS

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

    Proceedings of the 18th Nordic Workshop on Programming Theory (NWPT'06) 2 pp. total Reykjavík, Iceland

    We describe Nominal Structured Operational Semantics, a framework for specifying operational semantics within which proofs of congruence are carried out ‘once and for all’.

  4. Publication type: Conference paper
    SOS for Higher Order Processes (Extended Abstract)

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

    Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05) eds. Abadi, Martin; de Alfaro, Luca Lecture Notes in Computer Science vol. 3653 pp. 308–322 Springer

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

  5. Publication type: Book chapter
    The π-Calculus in FM

    Murdoch J. Gabbay

    Thirty-five years of Automating Mathematics ed. Fairouz D. Kamareddine Applied Logic Series vol. 28 pp. 247–269 Dordrecht: Kluwer Academic Publishers edition 1 ISBN 978-1-4020-1656-1 eISBN 978-94-017-0253-9

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

  6. Publication type: Conference paper
    FreshML: Programming with Binders Made Simple

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

    SIGPLAN Notices vol. 38 pp. 263–274 ACM Press

    ML enriched with Gabbay-Pitts atoms-abstraction and nominal name-generation and pattern-matching.

  7. Publication type: Conference paper
Rewriting and unification 22 publications
  1. Publication type: Conference paper
    Equational Reasoning in Languages with Binders via Permutation Fixed-Points

    Ali K. Caires-Santos, Maribel Fernández, Murdoch James Gabbay, Daniele Nantes-Sobrinho

    11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026) ed. Frank Pfenning Leibniz International Proceedings in Informatics (LIPIcs) vol. 378 pp. 10:1–10:23 article 10 Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik ISBN 978-3-95977-433-8 ISSN 1868-8969

  2. Publication type: Journal article
    The language of Stratified Sets is confluent and strongly normalising

    Murdoch J. Gabbay

    Logical Methods in Computer Science vol. 14, no. 2 article 12

    Quine’s stratification condition viewed from the perspective of the theory of rewriting.

  3. Publication type: Journal article
    Checking Overlaps of Nominal Rewriting Rules

    Mauricio Ayala-Rincón, Maribel Fernández, Murdoch James Gabbay, Ana Cristina Rocha-Oliveira

    Electronic Notes in Theoretical Computer Science vol. 323 pp. 39–56 Elsevier B.V. ISSN 1571-0661

  4. Publication type: Journal article
    Meta-variables as infinite lists in nominal terms unification and rewriting

    Murdoch J. Gabbay

    Logic Journal of the IGPL vol. 20, no. 6 pp. 967–1000 Oxford University Press

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

  5. Publication type: Conference paper
    Principal Types for Nominal Theories

    Elliot Fairweather, Maribel Fernández, Murdoch J. Gabbay

    Proceedings of the 18th International Symposium on Fundamentals of Computation Theory (FCT 2011) eds. Olaf Owe, Martin Steffen, Jan Arne Telle Lecture Notes in Computer Science vol. 6914 pp. 160–172 Berlin, Heidelberg: Springer ISBN 978-3-642-22952-7 eISBN 978-3-642-22953-4

    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.

  6. Publication type: Journal article
    Permissive Nominal Terms and their Unification: an infinite, co-infinite approach to nominal techniques (journal version)

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

    Logic Journal of the IGPL vol. 18, no. 6 pp. 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.

  7. Publication type: Conference paper
    Closed nominal rewriting and efficiently computable nominal algebra equality

    Maribel Fernández, Murdoch J. Gabbay

    Electronic Proceedings in Theoretical Computer Science vol. 34 pp. 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.

  8. Publication type: Conference paper
    Permissive Nominal Terms and their Unification

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

    Atti del Convegno CILC 09: 24-esimo Convegno Italiano di Logica Computazionale eds. Marco Gavanelli, Fabrizio Riguzzi pp. 70–84 Ferrara, Italy: GULP (Italian Association for Logic Programming)

    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

  9. Publication type: Journal article
    A study of substitution, using nominal techniques and Fraenkel-Mostowski sets

    Murdoch J. Gabbay

    Theoretical Computer Science vol. 410, no. 12-13 pp. 1159–1189 Elsevier

    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.

  10. Publication type: Technical report
    Permissive Nominal Terms and their Unification

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

    School of Mathematical and Computer Sciences, Heriot-Watt University Technical Report no. HW-MACS-TR-0062 49 pp. total Edinburgh, UK

    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.

  11. Publication type: Technical report
    Permissive nominal terms

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

    INRIA Research Report no. RR-6682 15 pp. total Orsay, France

    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.

  12. Publication type: Journal article
    Capture-Avoiding Substitution as a Nominal Algebra

    Murdoch J. Gabbay, Aad Mathijssen

    Formal Aspects of Computing vol. 20, no. 4-5 pp. 451–479 Springer

    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.

  13. Publication type: Conference paper
    Substitution for Fraenkel-Mostowski foundations

    Murdoch J. Gabbay, Michael J. Gabbay

    Proceedings of the 2008 AISB Symposium on Computing and Philosophy AISB 2008 Convention: Communication, Interaction and Social Intelligence vol. 12 pp. 65–72 University of Aberdeen, Aberdeen, UK: The Society for the Study of Artificial Intelligence and Simulation of Behaviour ISBN 1-902956-71-0

    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.

  14. Publication type: Journal article
    Hierarchical Nominal Terms and Their Theory of Rewriting

    Murdoch J. Gabbay

    Electronic Notes in Theoretical Computer Science vol. 174, no. 5 pp. 37–52 Elsevier ISSN 1571-0661

    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.

  15. Publication type: Journal article
    Nominal rewriting (journal version)

    Maribel Fernández, Murdoch J. Gabbay

    Information and Computation vol. 205, no. 6 pp. 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.

  16. Publication type: Technical report
    Capture-Avoiding Substitution as a Nominal Algebra

    Murdoch J. Gabbay, Aad Mathijssen

    Heriot-Watt University HW-MACS-TR-0053

    Subsumed by “Capture-Avoiding Substitution as a Nominal Algebra”.

    Decidability and theory of models of a nominal algebra axiomatisation of capture-avoiding substitution.

  17. Publication type: Conference paper
    Capture-avoiding Substitution as a Nominal Algebra

    Murdoch J. Gabbay, Aad Mathijssen

    Proceedings of the 3rd International Colloquium on Theoretical Aspects of Computing (ICTAC 2006) Lecture Notes in Computer Science vol. 4281 pp. 198–212 Berlin: Springer

    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.

  18. Publication type: Conference paper
  19. Publication type: Conference paper
  20. Publication type: Journal article
    Nominal Unification

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

    Theoretical Computer Science vol. 323, no. 1–3 pp. 473–497 Essex, UK: Elsevier ISSN 0304-3975

    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.

  21. Publication type: Conference paper
    Nominal Rewriting Systems

    Maribel Fernández, Murdoch J. Gabbay, Ian Mackie

    Proceedings of the 6th ACM SIGPLAN symposium on Principles and Practice of Declarative Programming (PPDP 2004) pp. 108–119 ACM Press

    We generalise first-order rewriting with terms involving binding operations, using a nominal approach in which bound entities are explicitly named.

  22. Publication type: Conference paper
    Nominal Unification

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

    Proceedings of the 17th International Workshop on Computer Science Logic (CSL 2003) Lecture Notes in Computer Science vol. 2803 pp. 513–527 Springer

    See here for formal verification of the results Urban in Isabelle.

Semantics and duality 24 publications
  1. Publication type: Book chapter
    Decentralized Collaborative Action: Cryptoeconomics in Space

    Murdoch J. Gabbay

    Cryptoeconomic Theory eds. Melanie Swan, Soichiro Takagi, Frank Witte Advances in Science and Technology in the Age of AI vol. 1 pp. 53–70 Singapore: World Scientific ISBN 978-1-80061-865-7 eISBN 978-1-80061-867-1

  2. Publication type: Journal article
  3. Publication type: Preprint
  4. Publication type: Journal article
  5. Publication type: Journal article
  6. Publication type: Book
    Semitopology: Decentralised Collaborative Action via Topology, Algebra, and Logic

    Murdoch J. Gabbay

    Studies in Logic vol. 108 320 pp. total London: College Publications edition 1 ISBN 978-1-84890-465-1

  7. Publication type: Journal article
    Algebras of UTxO blockchains

    Murdoch J. Gabbay

    Mathematical Structures in Computer Science vol. 31, no. 9 In Homage to Martin Hofmann pp. 1034–1089 Cambridge University Press issue dated online

    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.

  8. Publication type: Journal article
    Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness

    Murdoch J. Gabbay, Michael J. Gabbay

    Annals of Pure and Applied Logic vol. 168, no. 3 pp. 501–621 Elsevier

    Everything you wanted to know about semantics of the lambda-calculus using nominal techniques.

  9. Publication type: Journal article
    Semantics out of context: nominal absolute denotations for first-order logic and computation

    Murdoch J. Gabbay

    Journal of the ACM vol. 63, no. 3 pp. 1–66 article 25 ISSN 1535-9921

    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.

  10. Publication type: Journal article
  11. Publication type: Book chapter
    Stone duality for First-Order Logic: a nominal approach

    Murdoch J. Gabbay

    HOWARD-60. A Festschrift on the Occasion of Howard Barringer's 60th Birthday eds. Andrei Voronkov, Margarita Korovina EPiC Series in Computing vol. 42 pp. 178–209 EasyChair

    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.

  12. Publication type: Journal article
    Imaginary groups: lazy monoids and reversible computation.

    Murdoch J. Gabbay, Peter Kropholler

    Mathematical Structures in Computer Science vol. 23, no. 05 pp. 1002–1031 Cambridge University Press

    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.

  13. Publication type: Journal article
    Denotation of contextual modal type theory (CMTT): syntax and meta-programming

    Murdoch J. Gabbay, Aleksandar Nanevski

    Journal of Applied Logic vol. 11, no. 1 pp. 1–29

    A denotation for CMTT. I wanted to understand this for years, and now we have an answer!

  14. Publication type: Journal article
    Game semantics in the nominal model

    Murdoch J. Gabbay, Dan R. Ghica

    Electronic Notes in Theoretical Computer Science vol. 286 Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012) pp. 173–189 Elsevier

    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.

  15. Publication type: Conference paper
    Nominal Semantics for Predicate Logic: Algebras, Substitution, Quantifiers, and Limits

    Gilles Dowek, Murdoch J. Gabbay

    Proceedings of the 9th Italian Convention on Computational Logic (CILC 2012) ed. Francesca A. Lisi CEUR workshop proceedings vol. 857 pp. 104–118 CEUR-WS.org

    Universal lattice properties used to specify top, meet, and forall as instances of a single notion of fresh-finite limit.

  16. Publication type: Preprint
  17. Publication type: Journal article
    Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables

    Murdoch J. Gabbay

    Mathematical Structures in Computer Science vol. 21, no. 5 pp. 997–1033 Cambridge University Press

    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.

  18. Publication type: Conference paper
    Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets

    Murdoch J. Gabbay, Dominic P. Mulligan

    Proceedings of the 6th International Workshop on Logical Frameworks and Meta-Languages (LFMTP 2011) EPTCS vol. 71 pp. 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.

  19. Publication type: Conference paper
    Stone duality for nominal Boolean algebras with NEW

    Murdoch J. Gabbay, Tadeusz Litak, Daniela Petrişan

    Proceedings of the 4th international conference on algebra and coalgebra in computer science (CALCO 2011) Lecture Notes in Computer Science vol. 6859 pp. 192–207 Springer ISBN 978-3-642-22943-5

    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.

  20. Publication type: Journal article
    Foundations of nominal techniques: logic and semantics of variables in abstract syntax

    Murdoch J. Gabbay

    Bulletin of Symbolic Logic vol. 17, no. 2 pp. 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.

  21. Publication type: Journal article
    A study of substitution, using nominal techniques and Fraenkel-Mostowski sets

    Murdoch J. Gabbay

    Theoretical Computer Science vol. 410, no. 12-13 pp. 1159–1189 Elsevier

    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.

  22. Publication type: Conference paper
    Nominal renaming sets

    Murdoch J. Gabbay, Martin Hofmann

    Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008) pp. 158–173 Springer

    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.

  23. Publication type: Conference paper
    Substitution for Fraenkel-Mostowski foundations

    Murdoch J. Gabbay, Michael J. Gabbay

    Proceedings of the 2008 AISB Symposium on Computing and Philosophy AISB 2008 Convention: Communication, Interaction and Social Intelligence vol. 12 pp. 65–72 University of Aberdeen, Aberdeen, UK: The Society for the Study of Artificial Intelligence and Simulation of Behaviour ISBN 1-902956-71-0

    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.

  24. Publication type: Technical report
    Nominal renaming sets

    Murdoch J. Gabbay

    Heriot-Watt University Technical Report no. HW-MACS-TR-0058 35 pp. total Edinburgh, UK

    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.

Semitopology and semiframes 5 publications
  1. Publication type: Book chapter
    Decentralized Collaborative Action: Cryptoeconomics in Space

    Murdoch J. Gabbay

    Cryptoeconomic Theory eds. Melanie Swan, Soichiro Takagi, Frank Witte Advances in Science and Technology in the Age of AI vol. 1 pp. 53–70 Singapore: World Scientific ISBN 978-1-80061-865-7 eISBN 978-1-80061-867-1

  2. Publication type: Journal article
  3. Publication type: Preprint
  4. Publication type: Journal article
  5. Publication type: Book
    Semitopology: Decentralised Collaborative Action via Topology, Algebra, and Logic

    Murdoch J. Gabbay

    Studies in Logic vol. 108 320 pp. total London: College Publications edition 1 ISBN 978-1-84890-465-1

BibTeX

Book

Cover of Semitopology by Murdoch J. Gabbay

College Publications · 2024

Semitopology

Decentralised Collaborative Action via Topology, Algebra, and Logic

Semitopologies provide a mathematical foundation for heterogeneous, decentralised, permissionless computing systems. Points stand for participants; open sets describe ways in which they can cooperate.

Published
August 2024
ISBN
978-1-84890-465-1

Talks

Thanks to the seminar organisers who gave me opportunities to present the ideas below, and thanks to all of those who made time to turn up.

Selected talks

  1. Talk type: Conference talk

    A declarative approach to specifying distributed algorithms using three-valued modal logic

    I discuss how to specify distributed protocols as axiomatic theories in three-valued modal logic. As usual for axiomatic (‘declarative’) specifications, this yields a compact, precise, easily-checkable summary of what the protocol is, while dispensing with algorithmic detail.

    Presented by Murdoch J. Gabbay 41st British Colloquium for Theoretical Computer Science (BCTCS 2025) Room TL325B, Learning and Teaching Building, University of Strathclyde Hosted by University of Strathclyde Glasgow, Scotland

  2. Talk type: Conference talk

    A shallow arithmetisation of first-order validity

    I discuss how to directly arithmetise (cryptographer-speak for ‘translate into polynomials, the language of cryptography’) validity over finite models. This means that you can specify a property – e.g. some desired correctness property – and via cryptographic magic generate succinct or zero-knowledge proofs that a model satisfies that correctness property, without communicating that model to the recipient of the proof. This is very useful, I would argue, for quickly proving correctness of data, behaviour, or anything else that can be finitely represented.

    Presented by Murdoch J. Gabbay 41st British Colloquium for Theoretical Computer Science (BCTCS 2025) Room TL325B, Learning and Teaching Building, University of Strathclyde Hosted by University of Strathclyde Glasgow, Scotland

  3. Talk type: Workshop talk

    Semitopologies and semiframes for distributed heterogeneous consensus

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open (this arises from modelling distributed systems). Semitopologies naturally generate a three-valued logic (by considering continuous functions out of them), and they can be dualised to semiframes, which are complete join-semilattices with a compatibility relation. We study these, along with various well-behavedness conditions on points in a semitopology.

    Presented by Murdoch J. Gabbay First Workshop on Heterogeneous Trust in Distributed Systems (HTDS 2023) Convocation Room 113, Friend Center Princeton, New Jersey, USA

  4. Talk type: Conference talk

    Nominal techniques as an Agda library

    Nominal techniques … in Agda! Proof-of-concept but a promising start. If you like this and want to develop it further or transfer the ideas to (say) Lean, then please get in touch.

    Presented by Orestis Melkonian With Murdoch J. Gabbay 29th International Conference on Types for Proofs and Programs (TYPES 2023) ETSI Informàtica, Universitat Politècnica de València Hosted by Universitat Politècnica de València Valencia, Spain

  5. Talk type: Course / lecture

    Nominal Datatypes in Haskell

    We demo my Nominal Datatypes Haskell package

    Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2020 (SPLV20) Laboratory for Foundations of Computer Science, University of Edinburgh Hosted by University of Edinburgh Online

    1. Nominal Datatypes in Haskell — Lecture 1 SPLV 2020 — Nominal datatypes Laboratory for Foundations of Computer Science, University of Edinburgh Online Recording for Nominal Datatypes in Haskell — Lecture 1
    2. Nominal Datatypes in Haskell — Lecture 2 SPLV 2020 — Nominal datatypes Laboratory for Foundations of Computer Science, University of Edinburgh Online Recording for Nominal Datatypes in Haskell — Lecture 2
    3. Nominal Datatypes in Haskell — Lecture 3 SPLV 2020 — Nominal datatypes Laboratory for Foundations of Computer Science, University of Edinburgh Online Recording for Nominal Datatypes in Haskell — Lecture 3
  6. Talk type: Seminar

    Topological nominal semantics

    Stone duality in a nominal universe.

    Thanks to Dan Marsden and Luke Ong. I outline two papers on algebraic and topological semantics for the lambda-calculus and first-order logic. See the announcement and abstract.

    OASIS seminar, Department of Computer Science, University of Oxford Oxford, UK

Full talks list

186 items, arranged by date.

Talks by date

2026

  1. Talk type: Course / lecture
    Distributed protocols: a logical approach

    Distributed protocols are famously hard to get right, specify, and reason about. Logic can help! For example, it can help us give a three-day summer school course on a message-free, time-free, failure-free logical abstraction for specifying message-passing timed protocols with failure.

    Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2026 (SPLV26) University of Glasgow Glasgow, Scotland

  2. Talk type: Research talk
    Exponential cake and consistent controllers

    This talk treats the consistent controllers problem: suppose you have multiple interacting state machines (controllers) A, B, C, and D. Suppose controller B is bad and might equivocate, meaning that it may report different and incompatible states to peers A, C, and D. How can peers A, C, and D detect this misbehaviour and gracefully recover to a consistent state? Answers that invoke a single controlling peer G that suspends A, C, and D and resets them to a most recent consistent state are not admissible; there is no deus ex machina here, just controllers trying to stay consistent. If this problem seems hypothetical – it’s not. The world already consists of interacting controllers and the problem of consistency is a serious brake on safe progress.

    Presented by Murdoch J. Gabbay With Isaac Sheff, Anthony Hart Heliax Research Talk

  3. Talk type: Workshop talk
    Declarative Bracha Broadcast using 3-valued logic

    Distributed protocols are typically described using imperative pseudocode. But what if we could specify them declaratively, as logical theories? We use a three-valued logic, where the third truth-value ‘b’ represents broken/Byzantine behaviour. The result is simple and highly effective.

    Presented by Murdoch J. Gabbay Epistemic logic and topological perspectives on distributed computing (CELT 2026) IRIF Paris, France

  4. Talk type: Workshop talk
    Heterogeneous Broadcast

    A protocol is heterogeneous when different controllers may have different trust assumptions. A controller is a machine that issues state: a bank, a national register, a blockchain, etc. The world has many controllers, each of which a) have their own trust assumptions and b) must interoperate with the others. Multiple trust assumptions takes us to a distinct design space, so that Heterogeneous Bracha Broadcast is not merely a generalisation of (Homogeneous) Bracha Broadcast: it’s a different beast.

    Presented by Murdoch J. Gabbay With Isaac Sheff Epistemic logic and topological perspectives on distributed computing (CELT 2026) IRIF Paris, France

  5. Talk type: Seminar
    Declarative distributed protocols using three-valued modal logic and semitopologies

    Distributed protocols are typically described using imperative pseudocode. But what if we could specify them declaratively, as logical theories? We use a three-valued logic, where the third truth-value ‘b’ represents broken/Byzantine behaviour, and semitopologies provide a language for describing quorums. The result is to exhibit protocols as simple and compact axiomatic theories.

    Presented by Murdoch J. Gabbay Paris Automata and Concurrency Theory Seminar Paris, France

  6. Talk type: Workshop talk
    Declarative distributed protocols using three-valued modal logic types

    I discuss how to specify distributed protocols as axiomatic theories in three-valued modal logic. As usual for axiomatic (‘declarative’) specifications, this yields a compact, precise, easily-checkable summary of what the protocol is, while dispensing with algorithmic detail.

    Presented by Murdoch J. Gabbay Dagstuhl Seminar 26071: Behavioural Types for Resilience Schloss Dagstuhl Dagstuhl, Germany

2025

  1. Talk type: Teaching talk
    Jamie’s musings and dubious advice

    I dispense dubious life advice to PhD students participating in the SPLV summer school. I can’t guarantee that the advice is sound, but I can guarantee that every mistake listed is one which I have personally seen made (mostly by myself). If only I had known then what I know now, well, I’d probably have made a whole different collection of mistakes. This talk was dedicated to the memory of Gilles Dowek, who was a colleague, friend, and most pertinently to this talk, an inexhaustible source of wise advice.

    Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2025 (SPLV25) University of Edinburgh Edinburgh, Scotland

  2. Talk type: Research talk
    Heterogeneous Broadcast

    I present Heterogeneous Bracha Broadcast; a broadcast protocol in which participants may have different trust assumptions (i.e. trust different sets of quorums). The name might suggest that Heterogeneous Bracha Broadcast is a generalisation of Bracha Broadcast, but it’s not really: introducing multiple quorum systems takes us into a new design space which (at least in this case) feels quite unlike the homogeneous case.

    Presented by Murdoch J. Gabbay With Isaac Sheff Against Cryptoeconomics Day

  3. Talk type: Research talk
    Heterogeneous Broadcast

    I present Heterogeneous Bracha Broadcast; a broadcast protocol in which participants may have different trust assumptions (i.e. trust different sets of quorums). The name might suggest that Heterogeneous Bracha Broadcast is a generalisation of Bracha Broadcast, but it’s not really: introducing multiple quorum systems takes us into a new design space which (at least in this case) feels quite unlike the homogeneous case.

    Presented by Murdoch J. Gabbay With Isaac Sheff Anoma Day

  4. Talk type: Conference talk
    A declarative approach to specifying distributed algorithms using three-valued modal logic

    I discuss how to specify distributed protocols as axiomatic theories in three-valued modal logic. As usual for axiomatic (‘declarative’) specifications, this yields a compact, precise, easily-checkable summary of what the protocol is, while dispensing with algorithmic detail.

    Presented by Murdoch J. Gabbay 41st British Colloquium for Theoretical Computer Science (BCTCS 2025) Room TL325B, Learning and Teaching Building, University of Strathclyde Hosted by University of Strathclyde Glasgow, Scotland

  5. Talk type: Conference talk
    A shallow arithmetisation of first-order validity

    I discuss how to directly arithmetise (cryptographer-speak for ‘translate into polynomials, the language of cryptography’) validity over finite models. This means that you can specify a property – e.g. some desired correctness property – and via cryptographic magic generate succinct or zero-knowledge proofs that a model satisfies that correctness property, without communicating that model to the recipient of the proof. This is very useful, I would argue, for quickly proving correctness of data, behaviour, or anything else that can be finitely represented.

    Presented by Murdoch J. Gabbay 41st British Colloquium for Theoretical Computer Science (BCTCS 2025) Room TL325B, Learning and Teaching Building, University of Strathclyde Hosted by University of Strathclyde Glasgow, Scotland

  6. Talk type: Workshop talk
    Message logic for service commitments

    Message logic is a logic for specifying and reasoning about promises that participants in a message-passing distributed system can make to one another. This sounds simple but it turns out to lead to a surprisingly nice logical framework. This logic is somewhat different from the logics I’m used to studying, notably because the notion of logical implication has a measure-theoretic flavour. This comes from the fact that promises made might be broken, even in good faith, e.g. if the entire network fails.

    Presented by Murdoch J. Gabbay IC3 Winter Retreat

2024

2023

  1. Talk type: Workshop talk
    Semitopologies and semiframes for distributed heterogeneous consensus

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open (this arises from modelling distributed systems). Semitopologies naturally generate a three-valued logic (by considering continuous functions out of them), and they can be dualised to semiframes, which are complete join-semilattices with a compatibility relation. We study these, along with various well-behavedness conditions on points in a semitopology.

    Presented by Murdoch J. Gabbay First Workshop on Heterogeneous Trust in Distributed Systems (HTDS 2023) Convocation Room 113, Friend Center Princeton, New Jersey, USA

  2. Talk type: Workshop talk
    Semitopology and (paraconsistent) logic

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open (this arises from modelling distributed systems). It turns out that semitopologies are most easily classified using a three-valued paraconsistent logic; put another way, when you try to develop a logic over semitopologies, with semantics as continuous functions, a third truth-value very naturally appears.

    Presented by Murdoch J. Gabbay Dagstuhl Seminar 23272: Epistemic and Topological Reasoning in Distributed Systems Schloss Dagstuhl Dagstuhl, Germany

  3. Talk type: Seminar
    Equivariance: the name of the true monster in your induction

    My PhD was all about difficulties encountered combining inductively defined syntax with variable binding. In this talk I make two arguments: first, that names are best considered a primitive datatype with specific mathematical properties; and second, that the specific property is fundamentally not the fancy stuff that most of my PhD was about, but instead it is the apparently bland assertion of equivariance, namely, the property that a name-permutation universally applied, preserves validity. Once you have equivariance, I argue, the rest of the theory drops out. Conversely, if you do not take equivariance as primitive, your treatment of names may become painful. In short: equivariance is it. For more on these ideas, see the associated paper, the Nominal Haskell package, and the Nominal Agda package.

    Presented by Murdoch J. Gabbay LAIV seminar

  4. Talk type: Conference talk
    Nominal techniques as an Agda library

    Nominal techniques … in Agda! Proof-of-concept but a promising start. If you like this and want to develop it further or transfer the ideas to (say) Lean, then please get in touch.

    Presented by Orestis Melkonian With Murdoch J. Gabbay 29th International Conference on Types for Proofs and Programs (TYPES 2023) ETSI Informàtica, Universitat Politècnica de València Hosted by Universitat Politècnica de València Valencia, Spain

  5. Talk type: Seminar
    Semitopology: a new topological model of heterogeneous consensus

    A quorum in a distributed system is a set of participants with sufficient power to take collective action, independently from the rest of the system. Quorums are closed under arbitrary union, but not under arbitrary intersection. It turns out that if you treat this as something that is nearly (but not quite) a point-set topology, and then replay topological notions like open set, closed set, dense set, and continuous function, interpreted as quorums, then you obtain constructs with real meaning in the theory of distributed systems (e.g. a dense set corresponds to a blocking set). It turns out further that if you take notions from distributed systems and view them topologically, then further rich structure is revealed.

    Presented by Murdoch J. Gabbay Scottish Programming Languages Seminar (SPLS) Coats Building, University of the West of Scotland Paisley, Scotland

  6. Talk type: Tech talk
    Karl Marx and the blockchain

    This talk is based on a book chapter on Karl Marx and the blockchain coauthored with Devraj Basu (which at least one reviewer really liked) and an article in the Times Higher Education. Marx was an economic thinker and a revolutionary, and it’s his economic thought that the talk and associated article focus on. The article unpacks a case for the relevance of Marxian economic thought to blockchain technology. Writing this was fun, and it was a nice change from pure mathematics.

    Presented by Murdoch J. Gabbay Huawei Tech Talk Edinburgh, UK

  7. Talk type: Colloquium
    A broadly Marxian analysis of blockchain and cryptocurrencies

    This talk is based on a book chapter on Karl Marx and the blockchain coauthored with Devraj Basu (which at least one reviewer really liked) and an article in the Times Higher Education. Marx was an economic thinker and a revolutionary, and it’s his economic thought that the talk and associated article focus on. The article unpacks a case for the relevance of Marxian economic thought to blockchain technology. Writing this was fun, and it was a nice change from pure mathematics.

    Presented by Murdoch J. Gabbay Middlesex Computer Science Colloquium

2022

  1. Talk type: Seminar
    The semitopology of heterogeneous consensus

    A mathematical notion of consensus in a heterogeneous permissionless environment. ‘Permissionless’ means that participants are free to join or leave the network without permission from a central authority; ‘heterogeneous’ means that participants may have different goals and beliefs.

    Thanks to the Online Social Choice and Welfare seminar series (permalink). Video online here.

    Online Social Choice and Welfare Seminar Online

  2. Talk type: Conference talk
    The (semi)topology of distributed consensus

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open. This generalises the notion of quorum from distributed systems. It soon becomes clear that the most interesting semitopologies are those that satisfy an intersection-of-open-sets property which is the precise negation of Hausdorff separation.

    Presented by Murdoch J. Gabbay 11th International Conference on Geometric and Topological Methods in Computer Science (GETCO 2022) EPITA School of Engineering and Computer Science Le Kremlin-Bicêtre, France / hybrid

  3. Talk type: Seminar
    An overview of my claimed proof of consistency of Quine's New Foundations (ConNF)

    As the title suggests. The claimed proof is here.

    Thanks to the LFCS seminar series. Video online here.

    LFCS seminar series, University of Edinburgh Edinburgh, UK

2021

2020

  1. Talk type: Course / lecture
    Nominal Datatypes in Haskell

    We demo my Nominal Datatypes Haskell package

    Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2020 (SPLV20) Laboratory for Foundations of Computer Science, University of Edinburgh Hosted by University of Edinburgh Online

    1. Nominal Datatypes in Haskell — Lecture 1 SPLV 2020 — Nominal datatypes Laboratory for Foundations of Computer Science, University of Edinburgh Online Recording for Nominal Datatypes in Haskell — Lecture 1
    2. Nominal Datatypes in Haskell — Lecture 2 SPLV 2020 — Nominal datatypes Laboratory for Foundations of Computer Science, University of Edinburgh Online Recording for Nominal Datatypes in Haskell — Lecture 2
    3. Nominal Datatypes in Haskell — Lecture 3 SPLV 2020 — Nominal datatypes Laboratory for Foundations of Computer Science, University of Edinburgh Online Recording for Nominal Datatypes in Haskell — Lecture 3

2019

2018

  1. Talk type: Seminar
    The language of stratified sets, Quine's NF, rewriting, and higher-order logic

    A somewhat meandering tour of some elementary and not-so-elementary results

    Thanks to Jessica Ryan. See the announcement and abstract.

    FATA seminar, Department of Computer Science, University of Glasgow Glasgow, UK

  2. Talk type: Seminar
    Topological nominal semantics

    Stone duality in a nominal universe.

    Thanks to Dan Marsden and Luke Ong. I outline two papers on algebraic and topological semantics for the lambda-calculus and first-order logic. See the announcement and abstract.

    OASIS seminar, Department of Computer Science, University of Oxford Oxford, UK

  3. Talk type: Workshop talk
    Equivariant ZFA with Choice (EZFAC)

    I argue for EZFAC as a foundation for nominal techniques.

    Thanks to the organisers for this lovely event. Here are the ARW conference proceedings, my poster, and my slides. A longer paper is here.

    Automated Reasoning Workshop 2018 Computer Laboratory, Cambridge, UK

2017

  1. Talk type: Course / lecture
    Technical writing

    A seminar given to local MSc students, on technical writing.

    MSc course, Heriot-Watt University Edinburgh, UK

2016

  1. Talk type: Conference talk
    Consistency of Quine's NF using nominal techniques

    My first time in Brussels. It seemed an extremly nice place and was surprisingly laid-back. The Highlights Conference was lovely and I will go next year (in London) if I can. In spite of the similar title, this talk was not a pure repeat of my talks at the Logic Colloquium in August (see below). Thanks to the Highlights Conference 2016, and to Slawomir Lasota for inviting me to speak in his session.

    Highlights Conference 2016 Brussels, Belgium

2015

  1. Talk type: Teaching talk
    On technical writing

    A talk given to MSc students on (you guessed it) technical writing. We teach CS students to do technical things, but rarely do we focus on how to communicate about technical things. This can lead to problems later on, so I feel that this is an important lack and it is one which I am always happy to try and address.

    Presented by Murdoch J. Gabbay MSc course, Heriot-Watt University Edinburgh, UK

2014

  1. Talk type: Seminar
    What sequent quantifier rules tell us about nominal semantics for logic

    A precis of parts of nominal semantics for predicate logic and semantics out of context.

    Thanks to the Leeds Logic Group.

    Leeds Logic Group, University of Leeds Leeds, UK

2013

  1. Talk type: Workshop talk
    Nominal duality theory for new, forall, and lambda

    I was privileged to be invited to the rather wonderful Dagstuhl seminar 13422 on Nominal Computation Theory in Dagstuhl, Germany.

    Thanks to the organisers for this great event. Shall we do another one?

    Dagstuhl Seminar 13422: Nominal Computation Theory Schloss Dagstuhl, Germany

  2. Talk type: Seminar
    An overview of nominal algebra, lattice, representation and dualities for computer science foundations

    Presentation at the Logic and Semantics Seminar in the Computer Lab, Cambridge. I discuss how nominal algebra and powersets naturally model first-order logic with equality and the lambda-calculus. We can base theories of lattices, algebra, and topology on these observations, extending the familiar style of Boolean and Heyting algebras and their representations and topologies.

    Thanks to Jonathan Hayman.

    Logic and Semantics Seminar, University of Cambridge Cambridge, UK

  3. Talk type: Seminar
    Denotation of Contextual Modal Type Theory

    Presentation at the Programming Research Group Seminar in the Computer Lab, Cambridge. See also the associated paper Denotation of … (a prize for the reader who guesses the rest of the title). Many thanks to Alan Mycroft and his team for being delightful and enthusiastic hosts.

    Programming Research Group Seminar, University of Cambridge Cambridge, UK

  4. Talk type: Conference talk
    Semantics of FOL and lambda-calculus using nominal techniques

    Presentation at the Samson@60 conference in honour of Samson Abramsky. Getting to this event was unusually challenging and so I have an unusually long list of kind, generous, and efficient people to thank for my being able to attend: thanks to Luke Ong, Prakash Pananganden, Dave Corne, and Destiny Chen.

    Samson@60 conference University of Oxford, UK

  5. Talk type: Seminar
    An informal survey of nominal techniques

    I sketch recent activity in nominal techniques and speculate on how nominal techniques could be useful in verification. The talk was aimed especially those not familiar with nominal techniques. I gave the talk without slides.

    IMDEA Software Institute Madrid, Spain

  6. Talk type: Seminar
    Denotation of Contextual Modal Type theory

    Nanevski in his PhD thesis introduced and studied Contextual Modal Theory Theory. This is a lambda-calculus based via the Curry-Howard correspondence on an extension of the modal logic S4 with multiple modalities, one for each variable. The application is to meta-programming, where the intuitive denotation of Box A is “syntax of type A”. The language itself is pretty, and we developed a denotational semantics with interesting properties. I will give a tour of the system and discuss future work. See also the paper on Denotations of CMTT. Thanks to César Sánchez and Aleksandar Nanevski, and thanks to Paola Huerta for the calm and efficient rescue from that first hotel.

    IMDEA Software Institute Madrid, Spain

2012

  1. Talk type: Workshop talk
    Stone duality for first-order logic, a nominal approach

    Presentation at the Workshop on Duality Theory in Algebra, Logic and Computer Science in the Mathematical Institute, Oxford. See also the associated paper Stone duality for first-order logic: a nominal approach to logic and topology. This was a particularly nice do, and a lovely chance for me to rub shoulders with a new community. One particular pleasure of the workshop was meeting a Polish academic who as a young man had studied with Mostowski. He told me some stories about the great man, and said how nice it was to see this mathematics being used.

    Workshop on Duality Theory in Algebra, Logic and Computer Science Mathematical Institute, Oxford, UK

  2. Talk type: Seminar
    Three semantics for logic out of context

    It is common to reason about semantics in a context. This context may be a valuation (assigning denotations to variables) or a typing context (assigning types to variables), or a memory state (enumerating known memory), and so on. I will outline a nominal approach to semantics which subsumes context into a more abstract nominal notion of support. Using this we can give three semantics to (first-order) logic: in lattices, sets, and algebras. The full details are technical and in this talk I will try to bring out the non-technical “meaning of it all”, with an emphasis (necessarily speculative, but realistic) on practical implications to logic, specification, and programming.

    Universidad Politécnica de Madrid Madrid, Spain

  3. Talk type: Seminar
    The algebraisation of logic using nominal techniques

    Over the past five years a number of systems, such as first-order logic and the lambda-calculus, have been algebraically axiomatised using nominal techniques. A next step is to relate these (equational) axiomatisations to order-theoretic notions such as complemented bounded lattices (a.k.a. Boolean algebras). I will talk about recent progress here, giving an order-theoretic account of first-order logic: the punchline is that it will correspond to a complemented finitely fresh-complete lattice with a substitution—wait for the talk or see my recent paper with Dowek Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits. Israel has a tradition in logical foundations. Fraenkel–the Fraenkel of Zermelo-Fraenkel and Fraenkel-Mostowski set theory–was Dean of Jerusalem University. So it was special while visiting the logic community in Israel to discover not only that they already knew the background to what I was talking about, but that also, their research had anticipated much of what I was about to say. Special thanks here to Arnon Avron.

    Tel Aviv University Tel Aviv, Israel

  4. Talk type: Seminar
    The application of symmetry to computing and meta-mathematics

    Symmetry has long been recognised as important in mathematics and physics, but its importance has been less appreciated in theories of logic and computation. In this (mathematically oriented, but non-technical) talk I describe what symmetry means in logic and computation, examine the benefits we can obtain by considering logic and computation as inherently “symmetric” mathematical entities, and relate this back to traditional foundations based on sets and functions. Special thanks here to Stuart Margolis and the remarkable Plotkin family.

    Bar-Ilan University Tel Aviv, Israel

2011

  1. Talk type: Workshop talk
    Stone duality for first-order logic, a nominal approach

    Given at the Howard Barringer workshop. Not a repeat of my talks at Paris or Edinburgh (see below), because I only had 20 minutes. Few technical details, much more discussion of the “conceptual stack” of nominal techniques and how I plan to develop the field. A very nice and interesting event with many varied speakers. The Festschrift is where the accompanying paper appears.

    Howard Barringer workshop, University of Manchester Manchester, UK

  2. Talk type: Seminar
    Stone duality for first-order logic, a nominal approach

    A talk given at the work group on Types and Realisability / Théorie des types et réalisabilité”. A repeat of my talk of the previous week in Edinburgh, but to a different audience (and getting a different set of very constructive comments). Interesting to present the same work to two different audiences and see the responses.

    Types and Realisability working group, INRIA Paris, France

  3. Talk type: Seminar
    Stone duality for first-order logic, a nominal approach

    Part of the LFCS seminar series in Edinburgh University. A brand-new duality result between appropriate nominal notions of topological space, and the nominal algebra axiomatisation of first-order logic from One-and-a-halfth order logic and Permissive-nominal logic.

    LFCS seminar series, University of Edinburgh Edinburgh, UK

  4. Talk type: Workshop talk
    Getting to the Box of it: proof-theory for meta-programming and modal type theory

    Talk given at the wonderful Roy Dyckhoff retirement event. I present new work with Aleksander Nanevski to give a denotational semantics to Contextual Modal Type Theory (CMTT).

    Roy Dyckhoff retirement event University of St Andrews, UK

  5. Talk type: Seminar
    Are all substitutions invertible; are all monoids groups?

    Talk given as part of the theoretical computer science seminars discussing how to injectively turn an arbitrary monoid into a group. Joint work with Peter Kropholler.

    Theoretical Computer Science Seminar, University of Birmingham Birmingham, UK

  6. Talk type: Workshop talk
    Nominal Henkin semantics

    Talk given at the 6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011). Joint work with Dominic Mulligan.

    6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011) Nijmegen, Netherlands

  7. Talk type: Conference talk
    Metamathematics based on nominal terms: first-order logics over nominal sets

    A talk given at British Colloquium for Theoretical Computer Science (BCTCS 2011) in Birmingham, UK. I discuss the application of nominal sets to designing metamathematical syntaxes.

    British Colloquium for Theoretical Computer Science (BCTCS 2011) Birmingham, UK

  8. Talk type: Workshop talk
    Metamathematics based on nominal terms and nominal logic: foundations of a nominal theorem-prover

    A talk given in the Automated Reasoning Workshop in Glasgow University, UK. I describe permissive nominal terms and their application in logic and algebra.

    Automated Reasoning Workshop University of Glasgow, UK

  9. Talk type: Seminar
    A gentle introduction to the shape of nominal techniques

    The same beginner-friendly talk I gave in February. I gave the talk on the whiteboard; there are no slides.

    University of Strathclyde Glasgow, UK

  10. Talk type: Seminar
    A gentle introduction to the shape of nominal techniques

    A beginner-friendly talk given at the University of Glasgow, UK on nominal techniques. The abstract and announcement are here. I gave the talk on the whiteboard; there are no slides.

    University of Glasgow Glasgow, UK

  11. Talk type: Seminar
    Nominal techniques, 2006-2011

    Given at Tel-Aviv university. I broadly survey of the development of nominal terms in logic since 2006 when I last visited the department, discussing permissive-nominal algebra and permissive-nominal logic. I gave the talk on the whiteboard; there are no slides.

    Tel Aviv University Tel Aviv, Israel

2010

  1. Talk type: Seminar
    Nominal techniques: logique, algèbre, calcul

    A talk given at the 16th meeting on Logic, Algebra, and Calculus at PPS in Paris, France. I talk about applications of nominal rewriting, algebra, and permissive-nominal logic to specifying and reasoning about logic, algebra, and calculus.

    Thanks to Delia Kesner and DIGITEO.

    16th meeting on Logic, Algebra, and Calculus, PPS Paris, France

  2. Talk type: Workshop talk
    Closed nominal rewriting and efficiently computable nominal algebra equality

    A talk given at the 5th International Workshop on Logical Frameworks and Meta-languages (LFMTP 2010) in Edinburgh, UK. I discuss the connection between nominal rewriting and nominal algebra. Joint work with Maribel Fernández.

    5th International Workshop on Logical Frameworks and Meta-languages (LFMTP 2010) Edinburgh, UK

  3. Talk type: Workshop talk
    Kripke-style models in which logic and computation have equal standing

    I discuss Kripke models of the untyped lambda-calculus at the lovely and exciting meeting in honour of Dana Scott.

    Scott in Scotland meeting, University of Edinburgh Edinburgh, UK

2009

  1. Talk type: Workshop talk
    Names: I denote, therefore I am

    A talk given at the SICSA Complex Systems Engineering Joint THREADSS/SEMANTICS Meeting in Scotland, UK. I discuss in general (philosophical?) terms some of the ideas and motivations underlying my research.

    Thanks to Phil Trinder.

    SICSA Complex Systems Engineering Joint THREADSS/SEMANTICS Meeting Heriot-Watt University, Edinburgh, UK

  2. Talk type: Course / lecture
    Nominal techniques: a theory of names and binding

    A series of three 90 minute talks on nominal techniques given at the Universidad Complutense in Madrid, Spain. I used the whiteboard; there are no slides.

    Thanks to Yolanda Ortega Mallen.

    Universidad Complutense de Madrid Madrid, Spain

    1. Nominal techniques: a theory of names and binding 6–22 October 2009 (three 90-minute lectures; individual dates not recorded) Nominal-techniques lecture series Universidad Complutense de Madrid Madrid, Spain
  3. Talk type: Conference talk
    Permissive nominal terms and their unification

    A talk given at CILC09, the 24th Italian Conference on Computational Logic in Ferrara, Italy. See also the associated paper. I discuss permissive-nominal terms, which are similar to nominal terms but with properties more like those of first-order syntax. In particular, permissive-nominal terms lack freshness contexts, have inherent notions of alpha-equivalence and ‘free atoms of’, and the notion of solution of a unification or matching problem is based just on substitution.

    24th Italian Conference on Computational Logic (CILC 2009) Ferrara, Italy

  4. Talk type: Workshop talk
    Semantic Nominal Terms

    A talk given at the 2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming in York, UK (a satellite event of ETAPS 2009). See also the associated paper. I discuss a semantics for nominal terms unknowns as ‘infinite streams of distinct atoms’. This reconciles atoms-abstraction with nominal terms. I also describe a form of substitution that is both capturing (as in nominal terms) and capture-avoiding (as in first-order syntax with binding) — at the same time.

    2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming University of York, UK

2008

  1. Talk type: Seminar
    The nature of sets in computer science

    A talk given at King’s College as part of their Advanced Programming Techniques seminar series, on Monday 29 September at 12:00. I show how from a belief in the empty set and in ordinals we can construct a mathematical universe large enough that mathematical objects (in particular, numbers, rationals, and reals) can be interpreted in it. In response to questions from the audience I discuss the difference between structure (which exists in the model) and meaning (which exists in our own minds). It was a pretty good audience!

    Advanced Programming Techniques Seminar, King's College London London, UK

  2. Talk type: Seminar
    Nominal terms and one-and-a-half level Curry Howard

    A talk given at the Cambridge University computer lab as part of their Logic and Semantics seminar series, on Friday 26 September at 2pm. Joint work with Dominic Mulligan.

    Logic and Semantics Seminar, University of Cambridge Cambridge, UK

  3. Talk type: Workshop talk
    Two-and-a-half order lambda-calculus

    Talk given on Friday 4 July in the WFLP 2008 in Italy at 10:00. I describe two-and-a-half order lambda-calculus, a two-level lambda-calculus. Normally, the lambda-calculus has a capture-avoiding substitution. The two-level lambda-calculus is actually two lambda calculi, with distinct namespaces for variable symbols of `strong’ and `weak’ variables, but sharing a common application operator. Substitution for a strong variable does not avoid capture by lambda-abstraction for a weak variable. This leads to interesting and unusual phenomena.

    Workshop on Functional and Logic Programming (WFLP 2008) Siena, Italy

  4. Talk type: Conference talk
    Substitution for Fraenkel-Mostowski Foundations

    Talk given on Friday 4 April in the AISB conference in Aberdeen at 17:30. I describe a substitution action defined for the atoms on Fraenkel-Mostowski sets (the general set theory version of nominal sets). In the original Gabbay-Pitts ‘nominal’ approach to modelling syntax, the atoms in Fraenkel-Mostowski set theory were used to model variable symbols. Since they have a substitution action, it may be that they can be used to model variables, as well. Joint work with Michael Gabbay. The associated paper is here.

    AISB Convention University of Aberdeen, UK

  5. Talk type: Workshop talk
    Arbitrary objects in mathematics and semantics

    Talk delivered by Michael Gabbay in the Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics on Thursday February 28. This talk was delivered by my co-author Michael Gabbay; a photo of Michael delivering the talk is online here. We connect relatively recent developments in Fraenkel-Mostowski sets and nominal style semantics, with existing philosophical thinking on arbitrary-ness and unknown entities in language, mathematics, and semantics. Joint work with Michael Gabbay. The associated paper is here.

    Presented by Michael Gabbay Arché workshop on abstract objects in semantics and the philosophy of mathematics Paris, France

  6. Talk type: Colloquium
    Term sequent logics: cut your terms

    Sequents, entailments, and cut-elimination — applied to term rewriting and reduction.

    Presented by Michael Gabbay With Murdoch Gabbay Department of Computer Science colloquium King's College London, Department of Computer Science Hosted by King's College London London, UK

  7. Talk type: Teaching talk
    Strange but true! Second year undergraduates chat all night online about logic course

    A talk given as part of the Flexible Learning Talks series in Heriot-Watt University on Friday 11 January. Thanks to Nicole Cargill-Kipar.

    Flexible Learning Talks series, Heriot-Watt University Edinburgh, UK

2007

  1. Talk type: Workshop talk
    Names, computations, logics: the hole story.

    Given at the Mathematical Theories of Abstraction, Substitution and Naming in Computer Science in ICMS, Edinburgh on May 27 at 12:05. Thanks to the organisers Fernández, Pitts, and Stark. I describe my current take on ‘nominal techniques’.

    Mathematical Theories of Abstraction, Substitution and Naming in Computer Science ICMS, Edinburgh, UK

  2. Talk type: Teaching talk
    Strange but true! 2nd year undergraduates chat all night online about logic course.

    A talk given at the Flexible Learning Conference in Edinburgh at Heriot-Watt on May 18 at 14:05. I discuss my experience teaching the F22HO2 ‘formal specification’ course, and in particular the success of a message board I set up for the course, which attracted 1600 posts in five weeks and which remains active today. The video is the worst video in the history of worst videos. Sorry that I put the camera on the projector so it picked up the noise from the fan.

    Flexible Learning Conference, Heriot-Watt University Edinburgh, UK

  3. Talk type: Seminar
    Fraenkel-Mostowski atoms model variables as well as names

    A talk given at SPLS in Edinburgh on March 8 at 14:30. In this non-technical talk, we discuss a recent paper in which I exhibit a capture-avoiding substitution action on the Fraenkel-Mostowski sets universe. This suggests a new view of variables as denotational objects (names with a substitution action). Thanks to Kenneth MacKenzie.

    Scottish Programming Languages Seminar, University of Edinburgh Edinburgh, UK

  4. Talk type: Seminar
    Names and variables

    A talk given at City University on February 27 at 12:00. We discuss our research intentions to investigate denotations in which names are first-class denotational citizens; why one might want to do this, and how we are doing it. Thanks to Artur Garcez.

    City University London, UK

2006

  1. Talk type: Seminar
    Nominal Algebra: a NEW mathematics of variables

    A talk given at the LMU Institut für Informatik in Munich on December 6 at 16:00. We describe nominal algebra, its use to naturally represent meta-level reasoning on theories with binding, then concentrate on a nominal algebra axiomatisation of substitution and argue that ‘variable’ can be modelled as a ‘name plus substitution action’. Thanks to Martin Hofmann.

    Institut für Informatik, LMU Munich Munich, Germany

  2. Talk type: Workshop talk
    Substitution in Fraenkel-Mostowski sets

    Given at the Centre for Mathematical Studies as part of the Cameleon meeting on December 2 at 16:00. We show how the model of names given by atoms in Fraenkel-Mostowski sets can be extended with a substitution action to a model of variables. Thanks to Thomas Forster.

    Cameleon meeting, Centre for Mathematical Sciences, University of Cambridge Cambridge, UK

  3. Talk type: Workshop talk
    Nominal Algebra

    Presented by my PhD student Aad Mathijssen in the 18th Nordic Workshop on Programming Theory (NWPT06) at Reykjavík University in Iceland. The corresponding abstract is here.

    Presented by Aad Mathijssen 18th Nordic Workshop on Programming Theory Reykjavík University, Iceland

  4. Talk type: Workshop talk
    Nominal techniques: evolving the atom

    A talk given at the Scottish Theorem Proving meeting in the School of computer science. We give a position talk on nominal techniques considered useful as a means to generalise compositionality. Thanks to Phil Trinder and Rob Rothenberg.

    Scottish Theorem Proving meeting, University of St Andrews St Andrews, UK

  5. Talk type: Teaching talk
    The lambda-calculus

    A brief talk-ette (talk-chen, talk-ino) presented to test my presentation skills as part of the PGCAP course.

    PGCAP course, Heriot-Watt University Edinburgh, UK

  6. Talk type: Workshop talk
    Incomplete objects using the NEW calculus of contexts

    Given at the DREAM workshop of the mathematical reasoning group at Edinburgh University on September 1. We speculate on higher-order logic in the NEW calculus of contexts.

    DREAM workshop, University of Edinburgh Edinburgh, UK

  7. Talk type: Workshop talk
    Hierarchical nominal rewriting

    Kindly presented on my behalf by James Cheney at LFMTP06 in Seattle, USA on Wednesday 16 August 2006 at 10:30.

    Presented by James Cheney Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2006) Seattle, USA

  8. Talk type: Seminar
    Concrete models of nominal algebra substitution

    Presented at the CISA/LFCS seminar at Edinburgh University on Tuesday 13 June 2006 at 4pm in room 4.03. Thanks to Lucas Dixon. (See also a revised and extended version.)

    CISA/LFCS Seminar, University of Edinburgh Edinburgh, UK

  9. Talk type: Course / lecture
    Nominal algebra with applications

    Presented as part of a course in Tel-Aviv University in 210 Schreiber at 10:30 on Thursday 4 May. Thanks to Nachum Dershowitz. Presented again at the Tel-Aviv University computer science departmental seminar at 10:00 on Tuesday 9 May. Only got half way through thanks to diligent questioning; I will deliver the second half at 10:00 on Tuesday 16 May. See papers gabbay:noma for the first half, and gabbay:onaah for the second.

    Presented by Murdoch J. Gabbay Mini-course Tel Aviv University Tel Aviv, Israel

  10. Talk type: Seminar
    Functional programming and unification with meta-variables

    A research seminar given with the Babel group at the Universidad Politecnica de Madrid on March 31. We discuss our recent axiomatisation of substitution, and the NEW calculus of contexts, suggesting connections with logic programming and describing what we think might naturally be done next in this area. Thanks to Julio Marino.

    Babel Group Seminar, Universidad Politécnica de Madrid Madrid, Spain

  11. Talk type: Seminar
    Nominal: an overview

    Presented at the Departmental Seminar at the Universidad Politecnica de Madrid on March 31. We give an overview of (one large part of) our research, focussing on ‘nominal’. Thanks to Manuel Hermenegildo, Juan-Jose Moreno, and Jim Lipton for the invitation to visit.

    Departmental Seminar, Universidad Politécnica de Madrid Madrid, Spain

  12. Talk type: Workshop talk
    A concrete model of linearity and separation

    Presented at the Scottish Theorem Proving Meeting at Heriot-Watt University on March 17. We describe what we think is probably a uniform sets-based semantics for linear logic and bunched implications. Thanks to Andrew Ireland. I repeated this talk as a research seminar with the Babel group at the Universidad Politecnica de Madrid on March 28 with title “A concrete semantics for truth in bunched implications and linear logic?”. Thanks to Julio Marino.

    Scottish Theorem Proving Meeting, Heriot-Watt University Edinburgh, UK

    1. A concrete model of linearity and separation Scottish Theorem Proving Meeting Heriot-Watt University Edinburgh, UK Slides for A concrete model of linearity and separation
    2. A concrete semantics for truth in bunched implications and linear logic? Babel group research seminar Universidad Politécnica de Madrid Madrid, Spain Slides for A concrete semantics for truth in bunched implications and linear logic?
  13. Talk type: Colloquium
    Is substitution an abstract notion?

    Departmental colloquium of March 13. We describe an axiomatisation of substitution in ‘nominal style’ and discuss its set-based semantics. Thanks to Iman Poernomo.

    Departmental Colloquium, King's College London London, UK

  14. Talk type: Seminar
    Separation

    Departmental seminar given at Heriot-Watt on March 6. We report on joint work with Joe Wells in which we consider semantics for multiplicative and additive implication. Thanks to Lilia Georgieva.

    Departmental Seminar, Heriot-Watt University Edinburgh, UK

  15. Talk type: Course / lecture
    A NEW semantics of substitution

    Report on joint research carried out with two students, Samuel Rota Bulo and Andrea Marin, in the framework of a course taught in the University of Venice. Presented by the students on March 1. Thanks to their tutor Simonetta Balsamo.

    Presented by Samuel Rota Bulo and Andrea Marin University of Venice Venice, Italy

  16. Talk type: Seminar
    The NEW calculus of contexts

    Talk given at the Scottish Programming Languages Seminar on February 1. We describe the NEW calculus of contexts, a lambda-calculus which tries to understand the meta-level/object-level split. Thanks to Edwin Brady. (I gave similar talks in Turin, Italy and at PPDP05.)

    Scottish Programming Languages Seminar, University of St Andrews St Andrews, UK

  17. Talk type: Seminar
    Nominal techniques and the meta-level

    Talk given at Venice University on January 24. In reaction to the question “So what is it that you do?”, I give an initially non-technical description of the motivations (as I see them) for that part of my work to date which has to do with nominal techniques. Thanks to Annalisa Bossi.

    University of Venice Venice, Italy

  18. Talk type: Colloquium
    Nominal Rewriting

    Talk given at the computational logic colloquium at Innsbruck University on January 23. We describe nominal rewriting as a meta-level framework for specifying rewriting, which accurately reflects the instantiation behaviour of meta-level variables with respect to object-level binding. We then expatiate way over the time limit on the general context of our research. Thanks to Aart Middeldorp for inviting me and to Georg Moser for making it happen.

    Computational Logic Colloquium, University of Innsbruck Innsbruck, Austria

  19. Talk type: Workshop talk
    The NEW calculus of contexts

    Talk given at the Turin workshop on implicit computational complexity on January 19. We describe the NEW calculus of contexts, a lambda-calculus which tries to understand the meta-level/object-level split. Thanks to Simona Ronchi della Rocca. (A corrected and slightly modified version of a talk given at PPDP05.)

    Workshop on Implicit Computational Complexity, University of Turin Turin, Italy

  20. Talk type: Seminar
    The Fraenkel-Mostowski (FM) model of abstraction applied to name-generation

    Given at the ULTRA group seminar at Heriot-Watt on January 9. We discuss the FM model of abstraction, and briefly suggest its usefulness for both inductive and coinductive types. Thanks to Lilia Georgieva.

    ULTRA Group Seminar, Heriot-Watt University Edinburgh, UK

2005

  1. Talk type: Workshop talk
    Automating first-order logic

    Given at the second CANS meeting on December 6. We present Nominal Algebraic Specifications, a theory of universal algebra based on Nominal Terms and thus able to algebraically specify, in a suitable sense, theories-with-binding. We show how an algebraic theory of first-order logic leads to “one-and-a-halfth-order logic”, which is above first-order logic and slightly to the side of second-order logic. We discuss proof-methods for the system and possible extensions. Thanks to Maribel Fernández.

    Second CANS meeting, King's College London London, UK

  2. Talk type: Colloquium
    One-and-a-halfth-order logic

    Given at the Institute for Logic, Language, and Computation, in their colloquium on mathematical logic. We present one-and-a-halfth-order logic, which is a logic somewhere above first-order logic and slightly to the side of second-order logic. It satisfies cut-elimination, has an algebraic presentation, and allows to quantify over all predicates in an interesting and unusual way. Thanks to Benedikt Loewe.

    Mathematical Logic Colloquium, Institute for Logic, Language and Computation Utrecht University, Netherlands

  3. Talk type: Seminar
    Nominal Logic and FM techniques: reasoning about binding without pain

    Given at the Foundations Group seminar of the Brouwer Institute in Radboud University in Nijmegen on November 29. We give a relatively technical sketch of FM techniques, Nominal Logic, and their application to reasoning on syntax-with-binding. Thanks to Henk Barendregt and Bas Spitters. I gave the same talk at the Logic and Semantics Group Joint Theory seminar (‘Joint’ between Queen Mary and Westfield College and Imperial College) at Queen Mary and Westfield College on December 7 under the name “Fraenkel-Mostowski Techniques, a NEW model of freshness and abstraction”. Thanks to Peter O’Hearn. One member of the audience in Nijmegen then kindly invited me to give the talk again at the Theoretical Computer Science department in the Vrije Universiteit Amsterdam on December 12 (I used the original title). Thanks to Jan-Willem Klop and Femke van Raamsdonk.

    Foundations Group Seminar, Brouwer Institute Radboud University, Nijmegen, Netherlands

    1. Nominal Logic and FM techniques: reasoning about binding without pain Foundations Group seminar, Brouwer Institute Radboud University Nijmegen, Netherlands Slides for Nominal Logic and FM techniques: reasoning about binding without pain
    2. Fraenkel-Mostowski Techniques, a NEW model of freshness and abstraction Logic and Semantics Group Joint Theory seminar Queen Mary and Westfield College London, UK Slides for Fraenkel-Mostowski Techniques, a NEW model of freshness and abstraction
    3. Nominal Logic and FM techniques: reasoning about binding without pain Theoretical Computer Science seminar Vrije Universiteit Amsterdam Amsterdam, Netherlands Slides for Nominal Logic and FM techniques: reasoning about binding without pain
  4. Talk type: Seminar
    a-logic

    Talk given in the Logic Tea series at the University of Amsterdam on November 22. We discuss a-logic, a first-order logic with a predicate atom which is true of variable symbols and false of non-variable symbol terms. We axiomatise the untyped lambda-calculus by way of example and discuss what models look like, some possible future work, and the design decisions (and some of the sins) hidden in the paper. Thanks to Johan van Benthem and Olivier Roy.

    Logic Tea, University of Amsterdam Amsterdam, Netherlands

  5. Talk type: Seminar
    Nominal algebraic specifications

    Talk given at London South Bank University on November 8 and at University College London on November 9. We discuss Nominal Algebraic Specifications, an algebraic framework tailored to axiomatising systems-with-binding such as the lambda-calculus and logic. Thanks to Jonathan Bowen and Robin Hirsch.

    London South Bank University London, UK

    1. Nominal algebraic specifications Research seminar London South Bank University London, UK Slides for Nominal algebraic specifications
    2. Nominal algebraic specifications Research seminar University College London London, UK Slides for Nominal algebraic specifications
  6. Talk type: Workshop talk
    Nominal terms with a hierarchy of variables

    Bleeding-edge talk given in Eindhoven in a group workshop on 31 October 2005. We give a speculative account of an algebraic version of the NEW calculus of contexts.

    Group workshop, Eindhoven University of Technology Eindhoven, Netherlands

  7. Talk type: Conference talk
    Extended Nominal Rewriting: two models of binding

    Talk given at PPDP05 in Lisbon on 10 July 2005. We discuss two notions of binding which exist side-by-side in Extended Nominal Rewriting; one modelling lambda-calculus-like abstraction, the other modelling pi-calculus-like restriction. Some typos fixed with respect to the similar talk in Paris, and only 30 minutes long.

    Principles and Practice of Declarative Programming (PPDP 2005) Lisbon, Portugal

  8. Talk type: Conference talk
    A NEW calculus of contexts

    Talk given at PPDP05 in Lisbon on 10 July 2005. We discuss a lambda-calculus with a hierarchy of variables of different ‘strengths’ (corresponding roughly to increasingly ‘meta’ variables). We find it to be remarkably expressive, and suggest that we can encode records, modules, objects, dynamic binding and rebinding, and many other constructs involving non-capture-avoiding substitution.

    Principles and Practice of Declarative Programming (PPDP 2005) Lisbon, Portugal

  9. Talk type: Workshop talk
    Is there a quick way to get names and binding in some nominal sense up and running in Isabelle/HOL polymorphically on the type-class ‘type’, without having to rewrite the whole thing from scratch — yes or no?

    Talk given at the Binding Challenges workshop in JAIST, Ishikawa, Japan. Thanks to Rene Vestergaard. We speculate on an interesting way in which it may be possible to encode syntax-with-binding in a higher-order logic based theorem-proving environment.

    Binding Challenges workshop, Japan Advanced Institute of Science and Technology Ishikawa, Japan

  10. Talk type: Seminar
    Aspects of Nominal Rewriting

    Slides of a talk given at the CWI in Amsterdam on 2 March, and TUE in Eindhoven on 3 March. Thanks to Anton Wijs and MohammadReza Mousavi.

    CWI Amsterdam, Netherlands

    1. Aspects of Nominal Rewriting Research seminar Centrum Wiskunde & Informatica (CWI) Amsterdam, Netherlands Slides for Aspects of Nominal Rewriting
    2. Aspects of Nominal Rewriting Research seminar Eindhoven University of Technology Eindhoven, Netherlands Slides for Aspects of Nominal Rewriting
  11. Talk type: Seminar
    A NEW calculus of contexts

    Slides of a talk given in INRIA Rocquencourt Paris, on 21 February, and PPS Paris, on 22 February. Thanks to James Leifer, Russ Harmer, and the people of PPS and INRIA.

    INRIA Rocquencourt Paris, France

    1. A NEW calculus of contexts Research seminar INRIA Rocquencourt Paris, France Slides for A NEW calculus of contexts
    2. A NEW calculus of contexts Research seminar PPS Paris, France Slides for A NEW calculus of contexts

2004

  1. Talk type: Seminar
    Fresh Logic

    We discuss Fresh Logic (joint work with James Cheney) and consider its relation to FOLN a logic by Miller and Tiu, especially in the light of insights from implementation. Talk given to the PARCIFAL group at LIX on 14 May 2004.

    PARCIFAL Group, LIX Paris, France

  2. Talk type: Seminar
    Nominal Rewriting

    We present Nominal Rewriting, an essentially first-order rewriting system with inbuilt support for alpha-equivalence. See also “Incomplete lambda-terms” below. Talk given in LRI in their seminar series (27/2/2004, 10:30am).

    LRI Seminar France

  3. Talk type: Seminar
    Incomplete lambda-terms

    We use Nominal Rewriting to specify and discuss a lambda-calculus with meta-variables and explicit substitution. Talk given in LIX as part of a series of informal talks on meta-variables.

    LIX Paris, France

2003

  1. Talk type: Workshop talk
    Restart as a Computational Rule

    Talk given on applying the Curry-Howard correspondence to a novel Restart Logic. Given in the Workshop on Lambda Calculus, Type Theory, and Natural Language in King’s College London, on 9 December at 12:00 on work.

    Workshop on Lambda Calculus, Type Theory, and Natural Language King's College London, UK

  2. Talk type: Seminar
    FM binding for pi-calculus transitions

    Talk given on May 30 at Fundacao da Faculdade de Ciencias e Tecnologia / University of Lisbon. Thanks to Luis Caires and his department. See also an abstract.

    University of Lisbon Lisbon, Portugal

  3. Talk type: Seminar
    FM and the pi-calculus

    I investigate what happens if we consider an FM-like category of objects with a finite name-for-name renaming action (possibly non-injective maps between names) rather than a finite name-for-name permutation action as is the case for FM sets. I obtain a category similar to Schan, but which supports a natural interpretation of weak HOAS. Talk given on March 20 at the ENS Lyon, France. Thanks to Daniel Hirschkoff. See also an abstract.

    École Normale Supérieure de Lyon Lyon, France

  4. Talk type: Seminar
    FM for Higher-Order Abstract Syntax

    I investigate what happens if we consider an FM-like category of objects with a finite name-for-name renaming action (possibly non-injective maps between names) rather than a finite name-for-name permutation action as is the case for FM sets. I obtain a category similar to Schan, but which supports a natural interpretation of weak HOAS. Talk given on March 13 in Manchester University, thanks to Peter Aczel. See also an abstract.

    University of Manchester Manchester, UK

  5. Talk type: Seminar
    Restriction, binding, and three presentations of the pi-calculus

    I’ve been using FreshML to program a pet interest of mine; transition systems and bisimulation checkers for the pi-calculus (see [gabbay:thempc]). I’ll show excerpts from the programs I’ve written and talk about what writing them has taught me about another interest of mine; finding a semantics for restriction as distinct from binding. The sourcecode discussed is the pi-ltsb series of programs above, see [pi-ltsb] above.

    Semantics Lunch, University of Cambridge Cambridge, UK

2002

  1. Talk type: Seminar
    FM for Names and Binding

    Talk given on 11/12/2002 at the Japan Advanced Institute of Science and Technology, Ishikawa, on 14/12/2002 at MLG 2002 in Kinosaki, and on 16/12/2002 at ALGI in Kyoto. Thanks to René Vestergaard.

    Japan Advanced Institute of Science and Technology Ishikawa, Japan

    1. FM for Names and Binding Research seminar Japan Advanced Institute of Science and Technology Ishikawa, Japan Slides for FM for Names and Binding
    2. FM for Names and Binding MLG 2002 Kinosaki, Japan Slides for FM for Names and Binding
    3. FM for Names and Binding ALGI Kyoto, Japan Slides for FM for Names and Binding
  2. Talk type: Seminar
    FM Techniques for Syntax-with-Binding

    Talk given at INRIA Rocquencourt France 11/10/02 and Université Paris VII France 14/10/02. Thanks to Gilles Dowek and Pierre-Louis Curien.

    INRIA Rocquencourt and Université Paris VII Paris, France

    1. FM Techniques for Syntax-with-Binding Research seminar INRIA Rocquencourt Paris, France Slides for FM Techniques for Syntax-with-Binding
    2. FM Techniques for Syntax-with-Binding Research seminar Université Paris VII Paris, France Slides for FM Techniques for Syntax-with-Binding

Talks by topic

Some talks appear under more than one topic.

Algebra 9 talks
  1. Talk type: Seminar
    Are all substitutions invertible; are all monoids groups?

    Talk given as part of the theoretical computer science seminars discussing how to injectively turn an arbitrary monoid into a group. Joint work with Peter Kropholler.

    Theoretical Computer Science Seminar, University of Birmingham Birmingham, UK

  2. Talk type: Seminar
    Nominal Algebra: a NEW mathematics of variables

    A talk given at the LMU Institut für Informatik in Munich on December 6 at 16:00. We describe nominal algebra, its use to naturally represent meta-level reasoning on theories with binding, then concentrate on a nominal algebra axiomatisation of substitution and argue that ‘variable’ can be modelled as a ‘name plus substitution action’. Thanks to Martin Hofmann.

    Institut für Informatik, LMU Munich Munich, Germany

  3. Talk type: Workshop talk
    Nominal Algebra

    Presented by my PhD student Aad Mathijssen in the 18th Nordic Workshop on Programming Theory (NWPT06) at Reykjavík University in Iceland. The corresponding abstract is here.

    Presented by Aad Mathijssen 18th Nordic Workshop on Programming Theory Reykjavík University, Iceland

  4. Talk type: Seminar
    Concrete models of nominal algebra substitution

    Presented at the CISA/LFCS seminar at Edinburgh University on Tuesday 13 June 2006 at 4pm in room 4.03. Thanks to Lucas Dixon. (See also a revised and extended version.)

    CISA/LFCS Seminar, University of Edinburgh Edinburgh, UK

  5. Talk type: Course / lecture
    Nominal algebra with applications

    Presented as part of a course in Tel-Aviv University in 210 Schreiber at 10:30 on Thursday 4 May. Thanks to Nachum Dershowitz. Presented again at the Tel-Aviv University computer science departmental seminar at 10:00 on Tuesday 9 May. Only got half way through thanks to diligent questioning; I will deliver the second half at 10:00 on Tuesday 16 May. See papers gabbay:noma for the first half, and gabbay:onaah for the second.

    Presented by Murdoch J. Gabbay Mini-course Tel Aviv University Tel Aviv, Israel

  6. Talk type: Seminar
    Nominal algebraic specifications

    Talk given at London South Bank University on November 8 and at University College London on November 9. We discuss Nominal Algebraic Specifications, an algebraic framework tailored to axiomatising systems-with-binding such as the lambda-calculus and logic. Thanks to Jonathan Bowen and Robin Hirsch.

    London South Bank University London, UK

    1. Nominal algebraic specifications Research seminar London South Bank University London, UK Slides for Nominal algebraic specifications
    2. Nominal algebraic specifications Research seminar University College London London, UK Slides for Nominal algebraic specifications
Blockchain 4 talks
  1. Talk type: Tech talk
    Karl Marx and the blockchain

    This talk is based on a book chapter on Karl Marx and the blockchain coauthored with Devraj Basu (which at least one reviewer really liked) and an article in the Times Higher Education. Marx was an economic thinker and a revolutionary, and it’s his economic thought that the talk and associated article focus on. The article unpacks a case for the relevance of Marxian economic thought to blockchain technology. Writing this was fun, and it was a nice change from pure mathematics.

    Presented by Murdoch J. Gabbay Huawei Tech Talk Edinburgh, UK

  2. Talk type: Colloquium
    A broadly Marxian analysis of blockchain and cryptocurrencies

    This talk is based on a book chapter on Karl Marx and the blockchain coauthored with Devraj Basu (which at least one reviewer really liked) and an article in the Times Higher Education. Marx was an economic thinker and a revolutionary, and it’s his economic thought that the talk and associated article focus on. The article unpacks a case for the relevance of Marxian economic thought to blockchain technology. Writing this was fun, and it was a nice change from pure mathematics.

    Presented by Murdoch J. Gabbay Middlesex Computer Science Colloquium

Consensus and distributed systems 17 talks
  1. Talk type: Course / lecture
    Distributed protocols: a logical approach

    Distributed protocols are famously hard to get right, specify, and reason about. Logic can help! For example, it can help us give a three-day summer school course on a message-free, time-free, failure-free logical abstraction for specifying message-passing timed protocols with failure.

    Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2026 (SPLV26) University of Glasgow Glasgow, Scotland

  2. Talk type: Research talk
    Exponential cake and consistent controllers

    This talk treats the consistent controllers problem: suppose you have multiple interacting state machines (controllers) A, B, C, and D. Suppose controller B is bad and might equivocate, meaning that it may report different and incompatible states to peers A, C, and D. How can peers A, C, and D detect this misbehaviour and gracefully recover to a consistent state? Answers that invoke a single controlling peer G that suspends A, C, and D and resets them to a most recent consistent state are not admissible; there is no deus ex machina here, just controllers trying to stay consistent. If this problem seems hypothetical – it’s not. The world already consists of interacting controllers and the problem of consistency is a serious brake on safe progress.

    Presented by Murdoch J. Gabbay With Isaac Sheff, Anthony Hart Heliax Research Talk

  3. Talk type: Workshop talk
    Heterogeneous Broadcast

    A protocol is heterogeneous when different controllers may have different trust assumptions. A controller is a machine that issues state: a bank, a national register, a blockchain, etc. The world has many controllers, each of which a) have their own trust assumptions and b) must interoperate with the others. Multiple trust assumptions takes us to a distinct design space, so that Heterogeneous Bracha Broadcast is not merely a generalisation of (Homogeneous) Bracha Broadcast: it’s a different beast.

    Presented by Murdoch J. Gabbay With Isaac Sheff Epistemic logic and topological perspectives on distributed computing (CELT 2026) IRIF Paris, France

  4. Talk type: Workshop talk
    Declarative Bracha Broadcast using 3-valued logic

    Distributed protocols are typically described using imperative pseudocode. But what if we could specify them declaratively, as logical theories? We use a three-valued logic, where the third truth-value ‘b’ represents broken/Byzantine behaviour. The result is simple and highly effective.

    Presented by Murdoch J. Gabbay Epistemic logic and topological perspectives on distributed computing (CELT 2026) IRIF Paris, France

  5. Talk type: Seminar
    Declarative distributed protocols using three-valued modal logic and semitopologies

    Distributed protocols are typically described using imperative pseudocode. But what if we could specify them declaratively, as logical theories? We use a three-valued logic, where the third truth-value ‘b’ represents broken/Byzantine behaviour, and semitopologies provide a language for describing quorums. The result is to exhibit protocols as simple and compact axiomatic theories.

    Presented by Murdoch J. Gabbay Paris Automata and Concurrency Theory Seminar Paris, France

  6. Talk type: Workshop talk
    Declarative distributed protocols using three-valued modal logic types

    I discuss how to specify distributed protocols as axiomatic theories in three-valued modal logic. As usual for axiomatic (‘declarative’) specifications, this yields a compact, precise, easily-checkable summary of what the protocol is, while dispensing with algorithmic detail.

    Presented by Murdoch J. Gabbay Dagstuhl Seminar 26071: Behavioural Types for Resilience Schloss Dagstuhl Dagstuhl, Germany

  7. Talk type: Research talk
    Heterogeneous Broadcast

    I present Heterogeneous Bracha Broadcast; a broadcast protocol in which participants may have different trust assumptions (i.e. trust different sets of quorums). The name might suggest that Heterogeneous Bracha Broadcast is a generalisation of Bracha Broadcast, but it’s not really: introducing multiple quorum systems takes us into a new design space which (at least in this case) feels quite unlike the homogeneous case.

    Presented by Murdoch J. Gabbay With Isaac Sheff Against Cryptoeconomics Day

  8. Talk type: Research talk
    Heterogeneous Broadcast

    I present Heterogeneous Bracha Broadcast; a broadcast protocol in which participants may have different trust assumptions (i.e. trust different sets of quorums). The name might suggest that Heterogeneous Bracha Broadcast is a generalisation of Bracha Broadcast, but it’s not really: introducing multiple quorum systems takes us into a new design space which (at least in this case) feels quite unlike the homogeneous case.

    Presented by Murdoch J. Gabbay With Isaac Sheff Anoma Day

  9. Talk type: Conference talk
    A declarative approach to specifying distributed algorithms using three-valued modal logic

    I discuss how to specify distributed protocols as axiomatic theories in three-valued modal logic. As usual for axiomatic (‘declarative’) specifications, this yields a compact, precise, easily-checkable summary of what the protocol is, while dispensing with algorithmic detail.

    Presented by Murdoch J. Gabbay 41st British Colloquium for Theoretical Computer Science (BCTCS 2025) Room TL325B, Learning and Teaching Building, University of Strathclyde Hosted by University of Strathclyde Glasgow, Scotland

  10. Talk type: Workshop talk
    Message logic for service commitments

    Message logic is a logic for specifying and reasoning about promises that participants in a message-passing distributed system can make to one another. This sounds simple but it turns out to lead to a surprisingly nice logical framework. This logic is somewhat different from the logics I’m used to studying, notably because the notion of logical implication has a measure-theoretic flavour. This comes from the fact that promises made might be broken, even in good faith, e.g. if the entire network fails.

    Presented by Murdoch J. Gabbay IC3 Winter Retreat

  11. Talk type: Workshop talk
    Semitopologies and semiframes for distributed heterogeneous consensus

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open (this arises from modelling distributed systems). Semitopologies naturally generate a three-valued logic (by considering continuous functions out of them), and they can be dualised to semiframes, which are complete join-semilattices with a compatibility relation. We study these, along with various well-behavedness conditions on points in a semitopology.

    Presented by Murdoch J. Gabbay First Workshop on Heterogeneous Trust in Distributed Systems (HTDS 2023) Convocation Room 113, Friend Center Princeton, New Jersey, USA

  12. Talk type: Workshop talk
    Semitopology and (paraconsistent) logic

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open (this arises from modelling distributed systems). It turns out that semitopologies are most easily classified using a three-valued paraconsistent logic; put another way, when you try to develop a logic over semitopologies, with semantics as continuous functions, a third truth-value very naturally appears.

    Presented by Murdoch J. Gabbay Dagstuhl Seminar 23272: Epistemic and Topological Reasoning in Distributed Systems Schloss Dagstuhl Dagstuhl, Germany

  13. Talk type: Seminar
    Semitopology: a new topological model of heterogeneous consensus

    A quorum in a distributed system is a set of participants with sufficient power to take collective action, independently from the rest of the system. Quorums are closed under arbitrary union, but not under arbitrary intersection. It turns out that if you treat this as something that is nearly (but not quite) a point-set topology, and then replay topological notions like open set, closed set, dense set, and continuous function, interpreted as quorums, then you obtain constructs with real meaning in the theory of distributed systems (e.g. a dense set corresponds to a blocking set). It turns out further that if you take notions from distributed systems and view them topologically, then further rich structure is revealed.

    Presented by Murdoch J. Gabbay Scottish Programming Languages Seminar (SPLS) Coats Building, University of the West of Scotland Paisley, Scotland

  14. Talk type: Seminar
    The semitopology of heterogeneous consensus

    A mathematical notion of consensus in a heterogeneous permissionless environment. ‘Permissionless’ means that participants are free to join or leave the network without permission from a central authority; ‘heterogeneous’ means that participants may have different goals and beliefs.

    Thanks to the Online Social Choice and Welfare seminar series (permalink). Video online here.

    Online Social Choice and Welfare Seminar Online

  15. Talk type: Conference talk
    The (semi)topology of distributed consensus

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open. This generalises the notion of quorum from distributed systems. It soon becomes clear that the most interesting semitopologies are those that satisfy an intersection-of-open-sets property which is the precise negation of Hausdorff separation.

    Presented by Murdoch J. Gabbay 11th International Conference on Geometric and Topological Methods in Computer Science (GETCO 2022) EPITA School of Engineering and Computer Science Le Kremlin-Bicêtre, France / hybrid

Declarative distributed protocols 9 talks
  1. Talk type: Course / lecture
    Distributed protocols: a logical approach

    Distributed protocols are famously hard to get right, specify, and reason about. Logic can help! For example, it can help us give a three-day summer school course on a message-free, time-free, failure-free logical abstraction for specifying message-passing timed protocols with failure.

    Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2026 (SPLV26) University of Glasgow Glasgow, Scotland

  2. Talk type: Research talk
    Exponential cake and consistent controllers

    This talk treats the consistent controllers problem: suppose you have multiple interacting state machines (controllers) A, B, C, and D. Suppose controller B is bad and might equivocate, meaning that it may report different and incompatible states to peers A, C, and D. How can peers A, C, and D detect this misbehaviour and gracefully recover to a consistent state? Answers that invoke a single controlling peer G that suspends A, C, and D and resets them to a most recent consistent state are not admissible; there is no deus ex machina here, just controllers trying to stay consistent. If this problem seems hypothetical – it’s not. The world already consists of interacting controllers and the problem of consistency is a serious brake on safe progress.

    Presented by Murdoch J. Gabbay With Isaac Sheff, Anthony Hart Heliax Research Talk

  3. Talk type: Workshop talk
    Heterogeneous Broadcast

    A protocol is heterogeneous when different controllers may have different trust assumptions. A controller is a machine that issues state: a bank, a national register, a blockchain, etc. The world has many controllers, each of which a) have their own trust assumptions and b) must interoperate with the others. Multiple trust assumptions takes us to a distinct design space, so that Heterogeneous Bracha Broadcast is not merely a generalisation of (Homogeneous) Bracha Broadcast: it’s a different beast.

    Presented by Murdoch J. Gabbay With Isaac Sheff Epistemic logic and topological perspectives on distributed computing (CELT 2026) IRIF Paris, France

  4. Talk type: Workshop talk
    Declarative Bracha Broadcast using 3-valued logic

    Distributed protocols are typically described using imperative pseudocode. But what if we could specify them declaratively, as logical theories? We use a three-valued logic, where the third truth-value ‘b’ represents broken/Byzantine behaviour. The result is simple and highly effective.

    Presented by Murdoch J. Gabbay Epistemic logic and topological perspectives on distributed computing (CELT 2026) IRIF Paris, France

  5. Talk type: Seminar
    Declarative distributed protocols using three-valued modal logic and semitopologies

    Distributed protocols are typically described using imperative pseudocode. But what if we could specify them declaratively, as logical theories? We use a three-valued logic, where the third truth-value ‘b’ represents broken/Byzantine behaviour, and semitopologies provide a language for describing quorums. The result is to exhibit protocols as simple and compact axiomatic theories.

    Presented by Murdoch J. Gabbay Paris Automata and Concurrency Theory Seminar Paris, France

  6. Talk type: Workshop talk
    Declarative distributed protocols using three-valued modal logic types

    I discuss how to specify distributed protocols as axiomatic theories in three-valued modal logic. As usual for axiomatic (‘declarative’) specifications, this yields a compact, precise, easily-checkable summary of what the protocol is, while dispensing with algorithmic detail.

    Presented by Murdoch J. Gabbay Dagstuhl Seminar 26071: Behavioural Types for Resilience Schloss Dagstuhl Dagstuhl, Germany

  7. Talk type: Research talk
    Heterogeneous Broadcast

    I present Heterogeneous Bracha Broadcast; a broadcast protocol in which participants may have different trust assumptions (i.e. trust different sets of quorums). The name might suggest that Heterogeneous Bracha Broadcast is a generalisation of Bracha Broadcast, but it’s not really: introducing multiple quorum systems takes us into a new design space which (at least in this case) feels quite unlike the homogeneous case.

    Presented by Murdoch J. Gabbay With Isaac Sheff Against Cryptoeconomics Day

  8. Talk type: Research talk
    Heterogeneous Broadcast

    I present Heterogeneous Bracha Broadcast; a broadcast protocol in which participants may have different trust assumptions (i.e. trust different sets of quorums). The name might suggest that Heterogeneous Bracha Broadcast is a generalisation of Bracha Broadcast, but it’s not really: introducing multiple quorum systems takes us into a new design space which (at least in this case) feels quite unlike the homogeneous case.

    Presented by Murdoch J. Gabbay With Isaac Sheff Anoma Day

  9. Talk type: Conference talk
    A declarative approach to specifying distributed algorithms using three-valued modal logic

    I discuss how to specify distributed protocols as axiomatic theories in three-valued modal logic. As usual for axiomatic (‘declarative’) specifications, this yields a compact, precise, easily-checkable summary of what the protocol is, while dispensing with algorithmic detail.

    Presented by Murdoch J. Gabbay 41st British Colloquium for Theoretical Computer Science (BCTCS 2025) Room TL325B, Learning and Teaching Building, University of Strathclyde Hosted by University of Strathclyde Glasgow, Scotland

Lambda calculus and metaprogramming 16 talks
  1. Talk type: Seminar
    Denotation of Contextual Modal Type Theory

    Presentation at the Programming Research Group Seminar in the Computer Lab, Cambridge. See also the associated paper Denotation of … (a prize for the reader who guesses the rest of the title). Many thanks to Alan Mycroft and his team for being delightful and enthusiastic hosts.

    Programming Research Group Seminar, University of Cambridge Cambridge, UK

  2. Talk type: Seminar
    Denotation of Contextual Modal Type theory

    Nanevski in his PhD thesis introduced and studied Contextual Modal Theory Theory. This is a lambda-calculus based via the Curry-Howard correspondence on an extension of the modal logic S4 with multiple modalities, one for each variable. The application is to meta-programming, where the intuitive denotation of Box A is “syntax of type A”. The language itself is pretty, and we developed a denotational semantics with interesting properties. I will give a tour of the system and discuss future work. See also the paper on Denotations of CMTT. Thanks to César Sánchez and Aleksandar Nanevski, and thanks to Paola Huerta for the calm and efficient rescue from that first hotel.

    IMDEA Software Institute Madrid, Spain

  3. Talk type: Workshop talk
    Getting to the Box of it: proof-theory for meta-programming and modal type theory

    Talk given at the wonderful Roy Dyckhoff retirement event. I present new work with Aleksander Nanevski to give a denotational semantics to Contextual Modal Type Theory (CMTT).

    Roy Dyckhoff retirement event University of St Andrews, UK

  4. Talk type: Workshop talk
    Nominal Henkin semantics

    Talk given at the 6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011). Joint work with Dominic Mulligan.

    6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011) Nijmegen, Netherlands

  5. Talk type: Workshop talk
    Two-and-a-half order lambda-calculus

    Talk given on Friday 4 July in the WFLP 2008 in Italy at 10:00. I describe two-and-a-half order lambda-calculus, a two-level lambda-calculus. Normally, the lambda-calculus has a capture-avoiding substitution. The two-level lambda-calculus is actually two lambda calculi, with distinct namespaces for variable symbols of `strong’ and `weak’ variables, but sharing a common application operator. Substitution for a strong variable does not avoid capture by lambda-abstraction for a weak variable. This leads to interesting and unusual phenomena.

    Workshop on Functional and Logic Programming (WFLP 2008) Siena, Italy

  6. Talk type: Teaching talk
    The lambda-calculus

    A brief talk-ette (talk-chen, talk-ino) presented to test my presentation skills as part of the PGCAP course.

    PGCAP course, Heriot-Watt University Edinburgh, UK

  7. Talk type: Workshop talk
    Incomplete objects using the NEW calculus of contexts

    Given at the DREAM workshop of the mathematical reasoning group at Edinburgh University on September 1. We speculate on higher-order logic in the NEW calculus of contexts.

    DREAM workshop, University of Edinburgh Edinburgh, UK

  8. Talk type: Seminar
    The NEW calculus of contexts

    Talk given at the Scottish Programming Languages Seminar on February 1. We describe the NEW calculus of contexts, a lambda-calculus which tries to understand the meta-level/object-level split. Thanks to Edwin Brady. (I gave similar talks in Turin, Italy and at PPDP05.)

    Scottish Programming Languages Seminar, University of St Andrews St Andrews, UK

  9. Talk type: Workshop talk
    The NEW calculus of contexts

    Talk given at the Turin workshop on implicit computational complexity on January 19. We describe the NEW calculus of contexts, a lambda-calculus which tries to understand the meta-level/object-level split. Thanks to Simona Ronchi della Rocca. (A corrected and slightly modified version of a talk given at PPDP05.)

    Workshop on Implicit Computational Complexity, University of Turin Turin, Italy

  10. Talk type: Conference talk
    A NEW calculus of contexts

    Talk given at PPDP05 in Lisbon on 10 July 2005. We discuss a lambda-calculus with a hierarchy of variables of different ‘strengths’ (corresponding roughly to increasingly ‘meta’ variables). We find it to be remarkably expressive, and suggest that we can encode records, modules, objects, dynamic binding and rebinding, and many other constructs involving non-capture-avoiding substitution.

    Principles and Practice of Declarative Programming (PPDP 2005) Lisbon, Portugal

  11. Talk type: Seminar
    A NEW calculus of contexts

    Slides of a talk given in INRIA Rocquencourt Paris, on 21 February, and PPS Paris, on 22 February. Thanks to James Leifer, Russ Harmer, and the people of PPS and INRIA.

    INRIA Rocquencourt Paris, France

    1. A NEW calculus of contexts Research seminar INRIA Rocquencourt Paris, France Slides for A NEW calculus of contexts
    2. A NEW calculus of contexts Research seminar PPS Paris, France Slides for A NEW calculus of contexts
  12. Talk type: Seminar
    Incomplete lambda-terms

    We use Nominal Rewriting to specify and discuss a lambda-calculus with meta-variables and explicit substitution. Talk given in LIX as part of a series of informal talks on meta-variables.

    LIX Paris, France

Logic and proof theory 37 talks
  1. Talk type: Conference talk
    A shallow arithmetisation of first-order validity

    I discuss how to directly arithmetise (cryptographer-speak for ‘translate into polynomials, the language of cryptography’) validity over finite models. This means that you can specify a property – e.g. some desired correctness property – and via cryptographic magic generate succinct or zero-knowledge proofs that a model satisfies that correctness property, without communicating that model to the recipient of the proof. This is very useful, I would argue, for quickly proving correctness of data, behaviour, or anything else that can be finitely represented.

    Presented by Murdoch J. Gabbay 41st British Colloquium for Theoretical Computer Science (BCTCS 2025) Room TL325B, Learning and Teaching Building, University of Strathclyde Hosted by University of Strathclyde Glasgow, Scotland

  2. Talk type: Seminar
    What sequent quantifier rules tell us about nominal semantics for logic

    A precis of parts of nominal semantics for predicate logic and semantics out of context.

    Thanks to the Leeds Logic Group.

    Leeds Logic Group, University of Leeds Leeds, UK

  3. Talk type: Seminar
    The algebraisation of logic using nominal techniques

    Over the past five years a number of systems, such as first-order logic and the lambda-calculus, have been algebraically axiomatised using nominal techniques. A next step is to relate these (equational) axiomatisations to order-theoretic notions such as complemented bounded lattices (a.k.a. Boolean algebras). I will talk about recent progress here, giving an order-theoretic account of first-order logic: the punchline is that it will correspond to a complemented finitely fresh-complete lattice with a substitution—wait for the talk or see my recent paper with Dowek Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits. Israel has a tradition in logical foundations. Fraenkel–the Fraenkel of Zermelo-Fraenkel and Fraenkel-Mostowski set theory–was Dean of Jerusalem University. So it was special while visiting the logic community in Israel to discover not only that they already knew the background to what I was talking about, but that also, their research had anticipated much of what I was about to say. Special thanks here to Arnon Avron.

    Tel Aviv University Tel Aviv, Israel

  4. Talk type: Conference talk
    Metamathematics based on nominal terms: first-order logics over nominal sets

    A talk given at British Colloquium for Theoretical Computer Science (BCTCS 2011) in Birmingham, UK. I discuss the application of nominal sets to designing metamathematical syntaxes.

    British Colloquium for Theoretical Computer Science (BCTCS 2011) Birmingham, UK

  5. Talk type: Workshop talk
    Metamathematics based on nominal terms and nominal logic: foundations of a nominal theorem-prover

    A talk given in the Automated Reasoning Workshop in Glasgow University, UK. I describe permissive nominal terms and their application in logic and algebra.

    Automated Reasoning Workshop University of Glasgow, UK

  6. Talk type: Seminar
    Nominal terms and one-and-a-half level Curry Howard

    A talk given at the Cambridge University computer lab as part of their Logic and Semantics seminar series, on Friday 26 September at 2pm. Joint work with Dominic Mulligan.

    Logic and Semantics Seminar, University of Cambridge Cambridge, UK

  7. Talk type: Colloquium
    Term sequent logics: cut your terms

    Sequents, entailments, and cut-elimination — applied to term rewriting and reduction.

    Presented by Michael Gabbay With Murdoch Gabbay Department of Computer Science colloquium King's College London, Department of Computer Science Hosted by King's College London London, UK

  8. Talk type: Workshop talk
    A concrete model of linearity and separation

    Presented at the Scottish Theorem Proving Meeting at Heriot-Watt University on March 17. We describe what we think is probably a uniform sets-based semantics for linear logic and bunched implications. Thanks to Andrew Ireland. I repeated this talk as a research seminar with the Babel group at the Universidad Politecnica de Madrid on March 28 with title “A concrete semantics for truth in bunched implications and linear logic?”. Thanks to Julio Marino.

    Scottish Theorem Proving Meeting, Heriot-Watt University Edinburgh, UK

    1. A concrete model of linearity and separation Scottish Theorem Proving Meeting Heriot-Watt University Edinburgh, UK Slides for A concrete model of linearity and separation
    2. A concrete semantics for truth in bunched implications and linear logic? Babel group research seminar Universidad Politécnica de Madrid Madrid, Spain Slides for A concrete semantics for truth in bunched implications and linear logic?
  9. Talk type: Seminar
    Separation

    Departmental seminar given at Heriot-Watt on March 6. We report on joint work with Joe Wells in which we consider semantics for multiplicative and additive implication. Thanks to Lilia Georgieva.

    Departmental Seminar, Heriot-Watt University Edinburgh, UK

  10. Talk type: Workshop talk
    Automating first-order logic

    Given at the second CANS meeting on December 6. We present Nominal Algebraic Specifications, a theory of universal algebra based on Nominal Terms and thus able to algebraically specify, in a suitable sense, theories-with-binding. We show how an algebraic theory of first-order logic leads to “one-and-a-halfth-order logic”, which is above first-order logic and slightly to the side of second-order logic. We discuss proof-methods for the system and possible extensions. Thanks to Maribel Fernández.

    Second CANS meeting, King's College London London, UK

  11. Talk type: Colloquium
    One-and-a-halfth-order logic

    Given at the Institute for Logic, Language, and Computation, in their colloquium on mathematical logic. We present one-and-a-halfth-order logic, which is a logic somewhere above first-order logic and slightly to the side of second-order logic. It satisfies cut-elimination, has an algebraic presentation, and allows to quantify over all predicates in an interesting and unusual way. Thanks to Benedikt Loewe.

    Mathematical Logic Colloquium, Institute for Logic, Language and Computation Utrecht University, Netherlands

  12. Talk type: Seminar
    a-logic

    Talk given in the Logic Tea series at the University of Amsterdam on November 22. We discuss a-logic, a first-order logic with a predicate atom which is true of variable symbols and false of non-variable symbol terms. We axiomatise the untyped lambda-calculus by way of example and discuss what models look like, some possible future work, and the design decisions (and some of the sins) hidden in the paper. Thanks to Johan van Benthem and Olivier Roy.

    Logic Tea, University of Amsterdam Amsterdam, Netherlands

  13. Talk type: Seminar
    Fresh Logic

    We discuss Fresh Logic (joint work with James Cheney) and consider its relation to FOLN a logic by Miller and Tiu, especially in the light of insights from implementation. Talk given to the PARCIFAL group at LIX on 14 May 2004.

    PARCIFAL Group, LIX Paris, France

  14. Talk type: Workshop talk
    Restart as a Computational Rule

    Talk given on applying the Curry-Howard correspondence to a novel Restart Logic. Given in the Workshop on Lambda Calculus, Type Theory, and Natural Language in King’s College London, on 9 December at 12:00 on work.

    Workshop on Lambda Calculus, Type Theory, and Natural Language King's College London, UK

Nominal techniques 40 talks
  1. Talk type: Seminar
    Equivariance: the name of the true monster in your induction

    My PhD was all about difficulties encountered combining inductively defined syntax with variable binding. In this talk I make two arguments: first, that names are best considered a primitive datatype with specific mathematical properties; and second, that the specific property is fundamentally not the fancy stuff that most of my PhD was about, but instead it is the apparently bland assertion of equivariance, namely, the property that a name-permutation universally applied, preserves validity. Once you have equivariance, I argue, the rest of the theory drops out. Conversely, if you do not take equivariance as primitive, your treatment of names may become painful. In short: equivariance is it. For more on these ideas, see the associated paper, the Nominal Haskell package, and the Nominal Agda package.

    Presented by Murdoch J. Gabbay LAIV seminar

  2. Talk type: Conference talk
    Nominal techniques as an Agda library

    Nominal techniques … in Agda! Proof-of-concept but a promising start. If you like this and want to develop it further or transfer the ideas to (say) Lean, then please get in touch.

    Presented by Orestis Melkonian With Murdoch J. Gabbay 29th International Conference on Types for Proofs and Programs (TYPES 2023) ETSI Informàtica, Universitat Politècnica de València Hosted by Universitat Politècnica de València Valencia, Spain

  3. Talk type: Course / lecture
    Nominal Datatypes in Haskell

    We demo my Nominal Datatypes Haskell package

    Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2020 (SPLV20) Laboratory for Foundations of Computer Science, University of Edinburgh Hosted by University of Edinburgh Online

    1. Nominal Datatypes in Haskell — Lecture 1 SPLV 2020 — Nominal datatypes Laboratory for Foundations of Computer Science, University of Edinburgh Online Recording for Nominal Datatypes in Haskell — Lecture 1
    2. Nominal Datatypes in Haskell — Lecture 2 SPLV 2020 — Nominal datatypes Laboratory for Foundations of Computer Science, University of Edinburgh Online Recording for Nominal Datatypes in Haskell — Lecture 2
    3. Nominal Datatypes in Haskell — Lecture 3 SPLV 2020 — Nominal datatypes Laboratory for Foundations of Computer Science, University of Edinburgh Online Recording for Nominal Datatypes in Haskell — Lecture 3
  4. Talk type: Seminar
    An informal survey of nominal techniques

    I sketch recent activity in nominal techniques and speculate on how nominal techniques could be useful in verification. The talk was aimed especially those not familiar with nominal techniques. I gave the talk without slides.

    IMDEA Software Institute Madrid, Spain

  5. Talk type: Seminar
    The application of symmetry to computing and meta-mathematics

    Symmetry has long been recognised as important in mathematics and physics, but its importance has been less appreciated in theories of logic and computation. In this (mathematically oriented, but non-technical) talk I describe what symmetry means in logic and computation, examine the benefits we can obtain by considering logic and computation as inherently “symmetric” mathematical entities, and relate this back to traditional foundations based on sets and functions. Special thanks here to Stuart Margolis and the remarkable Plotkin family.

    Bar-Ilan University Tel Aviv, Israel

  6. Talk type: Seminar
    A gentle introduction to the shape of nominal techniques

    The same beginner-friendly talk I gave in February. I gave the talk on the whiteboard; there are no slides.

    University of Strathclyde Glasgow, UK

  7. Talk type: Seminar
    A gentle introduction to the shape of nominal techniques

    A beginner-friendly talk given at the University of Glasgow, UK on nominal techniques. The abstract and announcement are here. I gave the talk on the whiteboard; there are no slides.

    University of Glasgow Glasgow, UK

  8. Talk type: Seminar
    Nominal techniques, 2006-2011

    Given at Tel-Aviv university. I broadly survey of the development of nominal terms in logic since 2006 when I last visited the department, discussing permissive-nominal algebra and permissive-nominal logic. I gave the talk on the whiteboard; there are no slides.

    Tel Aviv University Tel Aviv, Israel

  9. Talk type: Seminar
    Nominal techniques: logique, algèbre, calcul

    A talk given at the 16th meeting on Logic, Algebra, and Calculus at PPS in Paris, France. I talk about applications of nominal rewriting, algebra, and permissive-nominal logic to specifying and reasoning about logic, algebra, and calculus.

    Thanks to Delia Kesner and DIGITEO.

    16th meeting on Logic, Algebra, and Calculus, PPS Paris, France

  10. Talk type: Workshop talk
    Names: I denote, therefore I am

    A talk given at the SICSA Complex Systems Engineering Joint THREADSS/SEMANTICS Meeting in Scotland, UK. I discuss in general (philosophical?) terms some of the ideas and motivations underlying my research.

    Thanks to Phil Trinder.

    SICSA Complex Systems Engineering Joint THREADSS/SEMANTICS Meeting Heriot-Watt University, Edinburgh, UK

  11. Talk type: Course / lecture
    Nominal techniques: a theory of names and binding

    A series of three 90 minute talks on nominal techniques given at the Universidad Complutense in Madrid, Spain. I used the whiteboard; there are no slides.

    Thanks to Yolanda Ortega Mallen.

    Universidad Complutense de Madrid Madrid, Spain

    1. Nominal techniques: a theory of names and binding 6–22 October 2009 (three 90-minute lectures; individual dates not recorded) Nominal-techniques lecture series Universidad Complutense de Madrid Madrid, Spain
  12. Talk type: Workshop talk
    Names, computations, logics: the hole story.

    Given at the Mathematical Theories of Abstraction, Substitution and Naming in Computer Science in ICMS, Edinburgh on May 27 at 12:05. Thanks to the organisers Fernández, Pitts, and Stark. I describe my current take on ‘nominal techniques’.

    Mathematical Theories of Abstraction, Substitution and Naming in Computer Science ICMS, Edinburgh, UK

  13. Talk type: Seminar
    Fraenkel-Mostowski atoms model variables as well as names

    A talk given at SPLS in Edinburgh on March 8 at 14:30. In this non-technical talk, we discuss a recent paper in which I exhibit a capture-avoiding substitution action on the Fraenkel-Mostowski sets universe. This suggests a new view of variables as denotational objects (names with a substitution action). Thanks to Kenneth MacKenzie.

    Scottish Programming Languages Seminar, University of Edinburgh Edinburgh, UK

  14. Talk type: Seminar
    Names and variables

    A talk given at City University on February 27 at 12:00. We discuss our research intentions to investigate denotations in which names are first-class denotational citizens; why one might want to do this, and how we are doing it. Thanks to Artur Garcez.

    City University London, UK

  15. Talk type: Workshop talk
    Nominal techniques: evolving the atom

    A talk given at the Scottish Theorem Proving meeting in the School of computer science. We give a position talk on nominal techniques considered useful as a means to generalise compositionality. Thanks to Phil Trinder and Rob Rothenberg.

    Scottish Theorem Proving meeting, University of St Andrews St Andrews, UK

  16. Talk type: Seminar
    Nominal: an overview

    Presented at the Departmental Seminar at the Universidad Politecnica de Madrid on March 31. We give an overview of (one large part of) our research, focussing on ‘nominal’. Thanks to Manuel Hermenegildo, Juan-Jose Moreno, and Jim Lipton for the invitation to visit.

    Departmental Seminar, Universidad Politécnica de Madrid Madrid, Spain

  17. Talk type: Seminar
    Nominal techniques and the meta-level

    Talk given at Venice University on January 24. In reaction to the question “So what is it that you do?”, I give an initially non-technical description of the motivations (as I see them) for that part of my work to date which has to do with nominal techniques. Thanks to Annalisa Bossi.

    University of Venice Venice, Italy

  18. Talk type: Seminar
    The Fraenkel-Mostowski (FM) model of abstraction applied to name-generation

    Given at the ULTRA group seminar at Heriot-Watt on January 9. We discuss the FM model of abstraction, and briefly suggest its usefulness for both inductive and coinductive types. Thanks to Lilia Georgieva.

    ULTRA Group Seminar, Heriot-Watt University Edinburgh, UK

  19. Talk type: Seminar
    Nominal Logic and FM techniques: reasoning about binding without pain

    Given at the Foundations Group seminar of the Brouwer Institute in Radboud University in Nijmegen on November 29. We give a relatively technical sketch of FM techniques, Nominal Logic, and their application to reasoning on syntax-with-binding. Thanks to Henk Barendregt and Bas Spitters. I gave the same talk at the Logic and Semantics Group Joint Theory seminar (‘Joint’ between Queen Mary and Westfield College and Imperial College) at Queen Mary and Westfield College on December 7 under the name “Fraenkel-Mostowski Techniques, a NEW model of freshness and abstraction”. Thanks to Peter O’Hearn. One member of the audience in Nijmegen then kindly invited me to give the talk again at the Theoretical Computer Science department in the Vrije Universiteit Amsterdam on December 12 (I used the original title). Thanks to Jan-Willem Klop and Femke van Raamsdonk.

    Foundations Group Seminar, Brouwer Institute Radboud University, Nijmegen, Netherlands

    1. Nominal Logic and FM techniques: reasoning about binding without pain Foundations Group seminar, Brouwer Institute Radboud University Nijmegen, Netherlands Slides for Nominal Logic and FM techniques: reasoning about binding without pain
    2. Fraenkel-Mostowski Techniques, a NEW model of freshness and abstraction Logic and Semantics Group Joint Theory seminar Queen Mary and Westfield College London, UK Slides for Fraenkel-Mostowski Techniques, a NEW model of freshness and abstraction
    3. Nominal Logic and FM techniques: reasoning about binding without pain Theoretical Computer Science seminar Vrije Universiteit Amsterdam Amsterdam, Netherlands Slides for Nominal Logic and FM techniques: reasoning about binding without pain
  20. Talk type: Workshop talk
    Nominal terms with a hierarchy of variables

    Bleeding-edge talk given in Eindhoven in a group workshop on 31 October 2005. We give a speculative account of an algebraic version of the NEW calculus of contexts.

    Group workshop, Eindhoven University of Technology Eindhoven, Netherlands

  21. Talk type: Seminar
    FM for Names and Binding

    Talk given on 11/12/2002 at the Japan Advanced Institute of Science and Technology, Ishikawa, on 14/12/2002 at MLG 2002 in Kinosaki, and on 16/12/2002 at ALGI in Kyoto. Thanks to René Vestergaard.

    Japan Advanced Institute of Science and Technology Ishikawa, Japan

    1. FM for Names and Binding Research seminar Japan Advanced Institute of Science and Technology Ishikawa, Japan Slides for FM for Names and Binding
    2. FM for Names and Binding MLG 2002 Kinosaki, Japan Slides for FM for Names and Binding
    3. FM for Names and Binding ALGI Kyoto, Japan Slides for FM for Names and Binding
  22. Talk type: Seminar
    FM Techniques for Syntax-with-Binding

    Talk given at INRIA Rocquencourt France 11/10/02 and Université Paris VII France 14/10/02. Thanks to Gilles Dowek and Pierre-Louis Curien.

    INRIA Rocquencourt and Université Paris VII Paris, France

    1. FM Techniques for Syntax-with-Binding Research seminar INRIA Rocquencourt Paris, France Slides for FM Techniques for Syntax-with-Binding
    2. FM Techniques for Syntax-with-Binding Research seminar Université Paris VII Paris, France Slides for FM Techniques for Syntax-with-Binding
Process calculi 5 talks
  1. Talk type: Seminar
    FM binding for pi-calculus transitions

    Talk given on May 30 at Fundacao da Faculdade de Ciencias e Tecnologia / University of Lisbon. Thanks to Luis Caires and his department. See also an abstract.

    University of Lisbon Lisbon, Portugal

  2. Talk type: Seminar
    FM and the pi-calculus

    I investigate what happens if we consider an FM-like category of objects with a finite name-for-name renaming action (possibly non-injective maps between names) rather than a finite name-for-name permutation action as is the case for FM sets. I obtain a category similar to Schan, but which supports a natural interpretation of weak HOAS. Talk given on March 20 at the ENS Lyon, France. Thanks to Daniel Hirschkoff. See also an abstract.

    École Normale Supérieure de Lyon Lyon, France

  3. Talk type: Seminar
    Restriction, binding, and three presentations of the pi-calculus

    I’ve been using FreshML to program a pet interest of mine; transition systems and bisimulation checkers for the pi-calculus (see [gabbay:thempc]). I’ll show excerpts from the programs I’ve written and talk about what writing them has taught me about another interest of mine; finding a semantics for restriction as distinct from binding. The sourcecode discussed is the pi-ltsb series of programs above, see [pi-ltsb] above.

    Semantics Lunch, University of Cambridge Cambridge, UK

Programming languages 2 talks
Rewriting and unification 16 talks
  1. Talk type: Workshop talk
    Closed nominal rewriting and efficiently computable nominal algebra equality

    A talk given at the 5th International Workshop on Logical Frameworks and Meta-languages (LFMTP 2010) in Edinburgh, UK. I discuss the connection between nominal rewriting and nominal algebra. Joint work with Maribel Fernández.

    5th International Workshop on Logical Frameworks and Meta-languages (LFMTP 2010) Edinburgh, UK

  2. Talk type: Conference talk
    Permissive nominal terms and their unification

    A talk given at CILC09, the 24th Italian Conference on Computational Logic in Ferrara, Italy. See also the associated paper. I discuss permissive-nominal terms, which are similar to nominal terms but with properties more like those of first-order syntax. In particular, permissive-nominal terms lack freshness contexts, have inherent notions of alpha-equivalence and ‘free atoms of’, and the notion of solution of a unification or matching problem is based just on substitution.

    24th Italian Conference on Computational Logic (CILC 2009) Ferrara, Italy

  3. Talk type: Workshop talk
    Hierarchical nominal rewriting

    Kindly presented on my behalf by James Cheney at LFMTP06 in Seattle, USA on Wednesday 16 August 2006 at 10:30.

    Presented by James Cheney Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2006) Seattle, USA

  4. Talk type: Seminar
    Functional programming and unification with meta-variables

    A research seminar given with the Babel group at the Universidad Politecnica de Madrid on March 31. We discuss our recent axiomatisation of substitution, and the NEW calculus of contexts, suggesting connections with logic programming and describing what we think might naturally be done next in this area. Thanks to Julio Marino.

    Babel Group Seminar, Universidad Politécnica de Madrid Madrid, Spain

  5. Talk type: Colloquium
    Is substitution an abstract notion?

    Departmental colloquium of March 13. We describe an axiomatisation of substitution in ‘nominal style’ and discuss its set-based semantics. Thanks to Iman Poernomo.

    Departmental Colloquium, King's College London London, UK

  6. Talk type: Course / lecture
    A NEW semantics of substitution

    Report on joint research carried out with two students, Samuel Rota Bulo and Andrea Marin, in the framework of a course taught in the University of Venice. Presented by the students on March 1. Thanks to their tutor Simonetta Balsamo.

    Presented by Samuel Rota Bulo and Andrea Marin University of Venice Venice, Italy

  7. Talk type: Colloquium
    Nominal Rewriting

    Talk given at the computational logic colloquium at Innsbruck University on January 23. We describe nominal rewriting as a meta-level framework for specifying rewriting, which accurately reflects the instantiation behaviour of meta-level variables with respect to object-level binding. We then expatiate way over the time limit on the general context of our research. Thanks to Aart Middeldorp for inviting me and to Georg Moser for making it happen.

    Computational Logic Colloquium, University of Innsbruck Innsbruck, Austria

  8. Talk type: Conference talk
    Extended Nominal Rewriting: two models of binding

    Talk given at PPDP05 in Lisbon on 10 July 2005. We discuss two notions of binding which exist side-by-side in Extended Nominal Rewriting; one modelling lambda-calculus-like abstraction, the other modelling pi-calculus-like restriction. Some typos fixed with respect to the similar talk in Paris, and only 30 minutes long.

    Principles and Practice of Declarative Programming (PPDP 2005) Lisbon, Portugal

  9. Talk type: Seminar
    Aspects of Nominal Rewriting

    Slides of a talk given at the CWI in Amsterdam on 2 March, and TUE in Eindhoven on 3 March. Thanks to Anton Wijs and MohammadReza Mousavi.

    CWI Amsterdam, Netherlands

    1. Aspects of Nominal Rewriting Research seminar Centrum Wiskunde & Informatica (CWI) Amsterdam, Netherlands Slides for Aspects of Nominal Rewriting
    2. Aspects of Nominal Rewriting Research seminar Eindhoven University of Technology Eindhoven, Netherlands Slides for Aspects of Nominal Rewriting
  10. Talk type: Seminar
    Nominal Rewriting

    We present Nominal Rewriting, an essentially first-order rewriting system with inbuilt support for alpha-equivalence. See also “Incomplete lambda-terms” below. Talk given in LRI in their seminar series (27/2/2004, 10:30am).

    LRI Seminar France

Semantics and duality 13 talks
  1. Talk type: Seminar
    Topological nominal semantics

    Stone duality in a nominal universe.

    Thanks to Dan Marsden and Luke Ong. I outline two papers on algebraic and topological semantics for the lambda-calculus and first-order logic. See the announcement and abstract.

    OASIS seminar, Department of Computer Science, University of Oxford Oxford, UK

  2. Talk type: Workshop talk
    Nominal duality theory for new, forall, and lambda

    I was privileged to be invited to the rather wonderful Dagstuhl seminar 13422 on Nominal Computation Theory in Dagstuhl, Germany.

    Thanks to the organisers for this great event. Shall we do another one?

    Dagstuhl Seminar 13422: Nominal Computation Theory Schloss Dagstuhl, Germany

  3. Talk type: Seminar
    An overview of nominal algebra, lattice, representation and dualities for computer science foundations

    Presentation at the Logic and Semantics Seminar in the Computer Lab, Cambridge. I discuss how nominal algebra and powersets naturally model first-order logic with equality and the lambda-calculus. We can base theories of lattices, algebra, and topology on these observations, extending the familiar style of Boolean and Heyting algebras and their representations and topologies.

    Thanks to Jonathan Hayman.

    Logic and Semantics Seminar, University of Cambridge Cambridge, UK

  4. Talk type: Conference talk
    Semantics of FOL and lambda-calculus using nominal techniques

    Presentation at the Samson@60 conference in honour of Samson Abramsky. Getting to this event was unusually challenging and so I have an unusually long list of kind, generous, and efficient people to thank for my being able to attend: thanks to Luke Ong, Prakash Pananganden, Dave Corne, and Destiny Chen.

    Samson@60 conference University of Oxford, UK

  5. Talk type: Workshop talk
    Stone duality for first-order logic, a nominal approach

    Presentation at the Workshop on Duality Theory in Algebra, Logic and Computer Science in the Mathematical Institute, Oxford. See also the associated paper Stone duality for first-order logic: a nominal approach to logic and topology. This was a particularly nice do, and a lovely chance for me to rub shoulders with a new community. One particular pleasure of the workshop was meeting a Polish academic who as a young man had studied with Mostowski. He told me some stories about the great man, and said how nice it was to see this mathematics being used.

    Workshop on Duality Theory in Algebra, Logic and Computer Science Mathematical Institute, Oxford, UK

  6. Talk type: Seminar
    Three semantics for logic out of context

    It is common to reason about semantics in a context. This context may be a valuation (assigning denotations to variables) or a typing context (assigning types to variables), or a memory state (enumerating known memory), and so on. I will outline a nominal approach to semantics which subsumes context into a more abstract nominal notion of support. Using this we can give three semantics to (first-order) logic: in lattices, sets, and algebras. The full details are technical and in this talk I will try to bring out the non-technical “meaning of it all”, with an emphasis (necessarily speculative, but realistic) on practical implications to logic, specification, and programming.

    Universidad Politécnica de Madrid Madrid, Spain

  7. Talk type: Workshop talk
    Stone duality for first-order logic, a nominal approach

    Given at the Howard Barringer workshop. Not a repeat of my talks at Paris or Edinburgh (see below), because I only had 20 minutes. Few technical details, much more discussion of the “conceptual stack” of nominal techniques and how I plan to develop the field. A very nice and interesting event with many varied speakers. The Festschrift is where the accompanying paper appears.

    Howard Barringer workshop, University of Manchester Manchester, UK

  8. Talk type: Seminar
    Stone duality for first-order logic, a nominal approach

    A talk given at the work group on Types and Realisability / Théorie des types et réalisabilité”. A repeat of my talk of the previous week in Edinburgh, but to a different audience (and getting a different set of very constructive comments). Interesting to present the same work to two different audiences and see the responses.

    Types and Realisability working group, INRIA Paris, France

  9. Talk type: Seminar
    Stone duality for first-order logic, a nominal approach

    Part of the LFCS seminar series in Edinburgh University. A brand-new duality result between appropriate nominal notions of topological space, and the nominal algebra axiomatisation of first-order logic from One-and-a-halfth order logic and Permissive-nominal logic.

    LFCS seminar series, University of Edinburgh Edinburgh, UK

  10. Talk type: Workshop talk
    Kripke-style models in which logic and computation have equal standing

    I discuss Kripke models of the untyped lambda-calculus at the lovely and exciting meeting in honour of Dana Scott.

    Scott in Scotland meeting, University of Edinburgh Edinburgh, UK

  11. Talk type: Workshop talk
    Semantic Nominal Terms

    A talk given at the 2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming in York, UK (a satellite event of ETAPS 2009). See also the associated paper. I discuss a semantics for nominal terms unknowns as ‘infinite streams of distinct atoms’. This reconciles atoms-abstraction with nominal terms. I also describe a form of substitution that is both capturing (as in nominal terms) and capture-avoiding (as in first-order syntax with binding) — at the same time.

    2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming University of York, UK

  12. Talk type: Seminar
    FM for Higher-Order Abstract Syntax

    I investigate what happens if we consider an FM-like category of objects with a finite name-for-name renaming action (possibly non-injective maps between names) rather than a finite name-for-name permutation action as is the case for FM sets. I obtain a category similar to Schan, but which supports a natural interpretation of weak HOAS. Talk given on March 13 in Manchester University, thanks to Peter Aczel. See also an abstract.

    University of Manchester Manchester, UK

Semitopology and semiframes 9 talks
  1. Talk type: Workshop talk
    Declarative Bracha Broadcast using 3-valued logic

    Distributed protocols are typically described using imperative pseudocode. But what if we could specify them declaratively, as logical theories? We use a three-valued logic, where the third truth-value ‘b’ represents broken/Byzantine behaviour. The result is simple and highly effective.

    Presented by Murdoch J. Gabbay Epistemic logic and topological perspectives on distributed computing (CELT 2026) IRIF Paris, France

  2. Talk type: Seminar
    Declarative distributed protocols using three-valued modal logic and semitopologies

    Distributed protocols are typically described using imperative pseudocode. But what if we could specify them declaratively, as logical theories? We use a three-valued logic, where the third truth-value ‘b’ represents broken/Byzantine behaviour, and semitopologies provide a language for describing quorums. The result is to exhibit protocols as simple and compact axiomatic theories.

    Presented by Murdoch J. Gabbay Paris Automata and Concurrency Theory Seminar Paris, France

  3. Talk type: Workshop talk
    Semitopologies and semiframes for distributed heterogeneous consensus

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open (this arises from modelling distributed systems). Semitopologies naturally generate a three-valued logic (by considering continuous functions out of them), and they can be dualised to semiframes, which are complete join-semilattices with a compatibility relation. We study these, along with various well-behavedness conditions on points in a semitopology.

    Presented by Murdoch J. Gabbay First Workshop on Heterogeneous Trust in Distributed Systems (HTDS 2023) Convocation Room 113, Friend Center Princeton, New Jersey, USA

  4. Talk type: Workshop talk
    Semitopology and (paraconsistent) logic

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open (this arises from modelling distributed systems). It turns out that semitopologies are most easily classified using a three-valued paraconsistent logic; put another way, when you try to develop a logic over semitopologies, with semantics as continuous functions, a third truth-value very naturally appears.

    Presented by Murdoch J. Gabbay Dagstuhl Seminar 23272: Epistemic and Topological Reasoning in Distributed Systems Schloss Dagstuhl Dagstuhl, Germany

  5. Talk type: Seminar
    Semitopology: a new topological model of heterogeneous consensus

    A quorum in a distributed system is a set of participants with sufficient power to take collective action, independently from the rest of the system. Quorums are closed under arbitrary union, but not under arbitrary intersection. It turns out that if you treat this as something that is nearly (but not quite) a point-set topology, and then replay topological notions like open set, closed set, dense set, and continuous function, interpreted as quorums, then you obtain constructs with real meaning in the theory of distributed systems (e.g. a dense set corresponds to a blocking set). It turns out further that if you take notions from distributed systems and view them topologically, then further rich structure is revealed.

    Presented by Murdoch J. Gabbay Scottish Programming Languages Seminar (SPLS) Coats Building, University of the West of Scotland Paisley, Scotland

  6. Talk type: Seminar
    The semitopology of heterogeneous consensus

    A mathematical notion of consensus in a heterogeneous permissionless environment. ‘Permissionless’ means that participants are free to join or leave the network without permission from a central authority; ‘heterogeneous’ means that participants may have different goals and beliefs.

    Thanks to the Online Social Choice and Welfare seminar series (permalink). Video online here.

    Online Social Choice and Welfare Seminar Online

  7. Talk type: Conference talk
    The (semi)topology of distributed consensus

    A semitopology is like a topology, but without the restriction that an intersection of open sets needs to be open. This generalises the notion of quorum from distributed systems. It soon becomes clear that the most interesting semitopologies are those that satisfy an intersection-of-open-sets property which is the precise negation of Hausdorff separation.

    Presented by Murdoch J. Gabbay 11th International Conference on Geometric and Topological Methods in Computer Science (GETCO 2022) EPITA School of Engineering and Computer Science Le Kremlin-Bicêtre, France / hybrid

Set theory and foundations 20 talks
  1. Talk type: Seminar
    An overview of my claimed proof of consistency of Quine's New Foundations (ConNF)

    As the title suggests. The claimed proof is here.

    Thanks to the LFCS seminar series. Video online here.

    LFCS seminar series, University of Edinburgh Edinburgh, UK

  2. Talk type: Seminar
    The language of stratified sets, Quine's NF, rewriting, and higher-order logic

    A somewhat meandering tour of some elementary and not-so-elementary results

    Thanks to Jessica Ryan. See the announcement and abstract.

    FATA seminar, Department of Computer Science, University of Glasgow Glasgow, UK

  3. Talk type: Workshop talk
    Equivariant ZFA with Choice (EZFAC)

    I argue for EZFAC as a foundation for nominal techniques.

    Thanks to the organisers for this lovely event. Here are the ARW conference proceedings, my poster, and my slides. A longer paper is here.

    Automated Reasoning Workshop 2018 Computer Laboratory, Cambridge, UK

  4. Talk type: Conference talk
    Consistency of Quine's NF using nominal techniques

    My first time in Brussels. It seemed an extremly nice place and was surprisingly laid-back. The Highlights Conference was lovely and I will go next year (in London) if I can. In spite of the similar title, this talk was not a pure repeat of my talks at the Logic Colloquium in August (see below). Thanks to the Highlights Conference 2016, and to Slawomir Lasota for inviting me to speak in his session.

    Highlights Conference 2016 Brussels, Belgium

  5. Talk type: Seminar
    The nature of sets in computer science

    A talk given at King’s College as part of their Advanced Programming Techniques seminar series, on Monday 29 September at 12:00. I show how from a belief in the empty set and in ordinals we can construct a mathematical universe large enough that mathematical objects (in particular, numbers, rationals, and reals) can be interpreted in it. In response to questions from the audience I discuss the difference between structure (which exists in the model) and meaning (which exists in our own minds). It was a pretty good audience!

    Advanced Programming Techniques Seminar, King's College London London, UK

  6. Talk type: Conference talk
    Substitution for Fraenkel-Mostowski Foundations

    Talk given on Friday 4 April in the AISB conference in Aberdeen at 17:30. I describe a substitution action defined for the atoms on Fraenkel-Mostowski sets (the general set theory version of nominal sets). In the original Gabbay-Pitts ‘nominal’ approach to modelling syntax, the atoms in Fraenkel-Mostowski set theory were used to model variable symbols. Since they have a substitution action, it may be that they can be used to model variables, as well. Joint work with Michael Gabbay. The associated paper is here.

    AISB Convention University of Aberdeen, UK

  7. Talk type: Workshop talk
    Arbitrary objects in mathematics and semantics

    Talk delivered by Michael Gabbay in the Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics on Thursday February 28. This talk was delivered by my co-author Michael Gabbay; a photo of Michael delivering the talk is online here. We connect relatively recent developments in Fraenkel-Mostowski sets and nominal style semantics, with existing philosophical thinking on arbitrary-ness and unknown entities in language, mathematics, and semantics. Joint work with Michael Gabbay. The associated paper is here.

    Presented by Michael Gabbay Arché workshop on abstract objects in semantics and the philosophy of mathematics Paris, France

  8. Talk type: Workshop talk
    Substitution in Fraenkel-Mostowski sets

    Given at the Centre for Mathematical Studies as part of the Cameleon meeting on December 2 at 16:00. We show how the model of names given by atoms in Fraenkel-Mostowski sets can be extended with a substitution action to a model of variables. Thanks to Thomas Forster.

    Cameleon meeting, Centre for Mathematical Sciences, University of Cambridge Cambridge, UK

Teaching and technical communication 6 talks
  1. Talk type: Teaching talk
    Jamie’s musings and dubious advice

    I dispense dubious life advice to PhD students participating in the SPLV summer school. I can’t guarantee that the advice is sound, but I can guarantee that every mistake listed is one which I have personally seen made (mostly by myself). If only I had known then what I know now, well, I’d probably have made a whole different collection of mistakes. This talk was dedicated to the memory of Gilles Dowek, who was a colleague, friend, and most pertinently to this talk, an inexhaustible source of wise advice.

    Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2025 (SPLV25) University of Edinburgh Edinburgh, Scotland

  2. Talk type: Course / lecture
    Technical writing

    A seminar given to local MSc students, on technical writing.

    MSc course, Heriot-Watt University Edinburgh, UK

  3. Talk type: Teaching talk
    On technical writing

    A talk given to MSc students on (you guessed it) technical writing. We teach CS students to do technical things, but rarely do we focus on how to communicate about technical things. This can lead to problems later on, so I feel that this is an important lack and it is one which I am always happy to try and address.

    Presented by Murdoch J. Gabbay MSc course, Heriot-Watt University Edinburgh, UK

  4. Talk type: Teaching talk
    Strange but true! Second year undergraduates chat all night online about logic course

    A talk given as part of the Flexible Learning Talks series in Heriot-Watt University on Friday 11 January. Thanks to Nicole Cargill-Kipar.

    Flexible Learning Talks series, Heriot-Watt University Edinburgh, UK

  5. Talk type: Teaching talk
    Strange but true! 2nd year undergraduates chat all night online about logic course.

    A talk given at the Flexible Learning Conference in Edinburgh at Heriot-Watt on May 18 at 14:05. I discuss my experience teaching the F22HO2 ‘formal specification’ course, and in particular the success of a message board I set up for the course, which attracted 1600 posts in five weeks and which remains active today. The video is the worst video in the history of worst videos. Sorry that I put the camera on the projector so it picked up the noise from the fan.

    Flexible Learning Conference, Heriot-Watt University Edinburgh, UK

Theorem proving 1 talk
  1. Talk type: Workshop talk
    Is there a quick way to get names and binding in some nominal sense up and running in Isabelle/HOL polymorphically on the type-class ‘type’, without having to rewrite the whole thing from scratch — yes or no?

    Talk given at the Binding Challenges workshop in JAIST, Ishikawa, Japan. Thanks to Rene Vestergaard. We speculate on an interesting way in which it may be possible to encode syntax-with-binding in a higher-order logic based theorem-proving environment.

    Binding Challenges workshop, Japan Advanced Institute of Science and Technology Ishikawa, Japan

Software

I hope you find the following software interesting and perhaps informative. I enjoyed writing it.

Browser

Programmable slide-rule emulator

Explore a two-sided scientific slide rule with configurable scales, classic instrument layouts, and guided lessons. Move the slide and cursor, then save your own instrument for offline use.

Browser

Aperiodic Life

Cellular automata on square, hexagonal, Einstein-hat, and Penrose tilings. You can change the rules, paint a starting pattern, and watch the evolution of one of a library of curated examples. Some of those examples are new, including some novel glider shapes.

Tools

Scripts$

Small programs written when I remember that computers are supposed to save labour.

Recognition

“until just now I had thought the Booker Prize a rather trivial, showbizzy caper, but now I consider ... it a very serious, reliable indication of literary merit” - Kingsly Amis, on winning the Booker prize, "Memoirs" page 325

  1. Recognised in

    The Coinspondent · Friedemann Brenneis

    Named “Paper of the Year” by The Coinspondent

    Authors Devraj Basu and Murdoch J. Gabbay

    In a 31 July 2020 article for the German-language Bitcoin publication The Coinspondent, Friedemann Brenneis called the then-new arXiv preprint “the paper of the year”, praising its intelligence, pointed formulations, and thought-provoking analysis. Thank you! More reviews like this, please.

    Featured paper

    • Karl Marx and the Blockchain

      Devraj Basu and Murdoch J. Gabbay · arXiv:2007.13346 (July 2020); later published in Media, Technology and Education in a Post-Truth Society, 225–241 (2021)

  2. Recognised in

    ACM SIGLOG · EATCS · EACSL · Kurt Gödel Society

    Alonzo Church Award for Outstanding Contributions to Logic and Computation

    Recipients Murdoch J. Gabbay and Andrew M. Pitts

    Jointly awarded for introducing the theory of nominal representations: a mathematical framework for computation with atomic names, freshness, abstraction, binding, and scope.

    Works named in the award citation

  3. Recognised in

    Principles and Practice of Declarative Programming

    PPDP Most Influential Paper 10-Year Award

    Recipients Maribel Fernández, Murdoch J. Gabbay, and Ian Mackie

    Selected by the PPDP Steering Committee as the most influential paper from PPDP 2004, recognising its contribution to declarative programming and rewriting with names and binders.

    Recognised paper

Miscellaneous

If you cite my work, please use Murdoch J. Gabbay rather than M. J. Gabbay: my brother Mike has the same initials.


Editorial work

The Journal of Financial Technology is free and open-access, bringing together mathematics, statistics, computer science, finance, and law in fintech.



Food intolerance

I'm wheat-intolerant: I don't get an allergic reaction to wheat, but neither can I digest it, so it just sits in my digestion until it ... comes out, eventually.

Finding things to eat is not a problem, thank goodness, but I miss out on convenience. I can't just "grab a sandwich". I have to plan ahead, just in case.

  • I can eat non-wheat carbohydrates like rice, potatoes, oats, barley, corn, and rye. Porridge, polenta, and pumpernickel are fine.
  • Nuts, milk, and soya are not a problem.
  • I can't eat pasta, pizza, cous-cous (cracked grain), naan, laffa flatbreads, doughnuts, baguettes, croissants (which is a real pity), sandwiches, or saitan (purified wheat gluten; that one is a big no-no).
  • Potato gnocchi are fine; they contain a bit of wheat but it's generally not enough to bother me. Likewise, gravy thickened with a bit of wheat flour is fine. Funnily enough, I'm generally OK with a sinfully rich chocolate cake too: that's mostly sugar, fat, and chocolate, which I can digest very well.

I usually just ask for the "gluten-free" option. It's a simplification, but a useful one in practice.


Swedish Chef

For your convenience, my homepage is available in Swedish Chef (see Wikipedia and YouTube).