Decentralised systems
Semitopology, blockchain models and mathematical structures for cooperation without central control.
Mathematician, Logician, Academic, Computer scientist, Consultant, Lecturer, Editor
Everybody calls me Jamie.
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.
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.
Semitopology, blockchain models and mathematical structures for cooperation without central control.
Arithmetisation of first-order logic and cryptographic proofs over finite models.
A mathematical account of names, binding, freshness, and alpha-equivalence, grounded in nominal sets and the Gabbay–Pitts model.
The NEW quantifier
means “for a fresh name”
.
Nominal algebra, quantifiers, proof search, equational reasoning and the structure of logical derivations.
Mathematical models of logic and computation, including nominal semantics, lattices, topology and representation theorems.
Rewriting, substitution and unification in the presence of names, binding and alpha-equivalence.
Lambda-calculi, contexts, staged computation and syntax with meta-variables.
Programming with binders, types, operational semantics and process calculi.
Journal of Logic and Computation vol. 35, no. 5 article exae050 Oxford University Press online
Journal of Applied Logics vol. 12, no. 6 pp. 1481–1548 London: College Publications ISSN 2631-9810
Mathematical Structures in Computer Science vol. 31, no. 9 In Homage to Martin Hofmann pp. 1034–1089 Cambridge University Press issue dated online
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.
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.
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.
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.
108 items, arranged by date.
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
Anoma Research Topics Zenodo
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
Mathematical Structures in Computer Science vol. 36 article e3 Cambridge University Press
arXiv latest revision
Anoma Research Topics Zenodo
Journal of Applied Logics vol. 12, no. 6 pp. 1481–1548 London: College Publications ISSN 2631-9810
Journal of Logic and Computation vol. 35, no. 5 article exae050 Oxford University Press online
arXiv latest revision
Studies in Logic vol. 108 320 pp. total London: College Publications edition 1 ISBN 978-1-84890-465-1
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.
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
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.
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.
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.
Logical Methods in Computer Science vol. 14, no. 2 article 12
Quine’s stratification condition viewed from the perspective of the theory of rewriting.
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.
Electronic Notes in Theoretical Computer Science vol. 323 pp. 39–56 Elsevier B.V. ISSN 1571-0661
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.
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〉”.
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.
The IfCoLog Journal of Logics and their Applications vol. 1, no. 2 pp. 83–106 College Publications ISBN 978-1-84890-163-6 ISSN 2055-3706
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.
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.
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!
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.
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.
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
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.
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.
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.
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.
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.
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.
Subsumed by “Denotation of contextual modal type theory (CMTT): syntax and meta-programming”.
Automated Reasoning Workshop (ARW 2012) 2 pp. total
We consider liberalised delta-rules in proof-search, and give them a nominal algebraic semantics.
Subsumed by “PNL to HOL: from the logic of nominal sets to the logic of higher-order functions”.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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
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.
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.
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.
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.
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
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.
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.
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.
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.
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.
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.
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.
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.
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.
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).
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.
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.
Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics 2 pp. total Paris, France
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.
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).
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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’.
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.
Proceedings of LFMTP’06: First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice eds. Alberto Momigliano, Brigitte Pientka pp. 32–45 Seattle, Washington, USA
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.
Heriot-Watt University Technical Report no. HW-MACS-TR-0045 13 pp. total Edinburgh, UK
A detailed treatment of the nominal algebra presented in our abstract in NWPT06. Subsumed by a journal version.
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.
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.
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.)
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.
Proceedings of the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2005) pp. 47–58 ACM Press
We generalise and extend previous work on rewriting with variable binding, with name generation/restriction, and study its properties.
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.
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.
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.
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.
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.)
SIGPLAN Notices vol. 38 pp. 263–274 ACM Press
ML enriched with Gabbay-Pitts atoms-abstraction and nominal name-generation and pattern-matching.
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
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.
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.
Second Workshop on Meta-Logic (MLG 2002) 2 pp. total Kinosaki, Japan
A prose account of my talk at MLG02 in Kinosaki, Japan.
University of Cambridge Cambridge, UK
See also the survey paper on foundations on nominal techniques.
Proceedings of the 5th international conference on the mathematics of program construction (MPC 2000) Lecture Notes in Computer Science vol. 1837 pp. 230–255 Springer
Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS 1999) pp. 214–224 IEEE Computer Society Press
My first conference paper. See also the journal version.
Some publications appear under more than one topic.
Journal of Applied Logics vol. 12, no. 6 pp. 1481–1548 London: College Publications ISSN 2631-9810
Anoma Research Topics Zenodo
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
Mathematical Structures in Computer Science vol. 36 article e3 Cambridge University Press
arXiv latest revision
Anoma Research Topics Zenodo
Journal of Logic and Computation vol. 35, no. 5 article exae050 Oxford University Press online
arXiv latest revision
Studies in Logic vol. 108 320 pp. total London: College Publications edition 1 ISBN 978-1-84890-465-1
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.
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
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.
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.
Anoma Research Topics Zenodo
arXiv latest revision
Anoma Research Topics Zenodo
arXiv latest revision
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.
The IfCoLog Journal of Logics and their Applications vol. 1, no. 2 pp. 83–106 College Publications ISBN 978-1-84890-163-6 ISSN 2055-3706
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!
Subsumed by “Denotation of contextual modal type theory (CMTT): syntax and meta-programming”.
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.
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.
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.
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.
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.
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.
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.
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.
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).
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).
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.
arXiv latest revision
Journal of Applied Logics vol. 12, no. 6 pp. 1481–1548 London: College Publications ISSN 2631-9810
arXiv latest revision
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.
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.
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.
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.
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.
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.
Automated Reasoning Workshop (ARW 2012) 2 pp. total
We consider liberalised delta-rules in proof-search, and give them a nominal algebraic semantics.
Subsumed by “PNL to HOL: from the logic of nominal sets to the logic of higher-order functions”.
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.
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.
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.
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.
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
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.
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.
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.
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.
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).
Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics 2 pp. total Paris, France
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.
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.
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.
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.
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.
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.
Heriot-Watt University Technical Report no. HW-MACS-TR-0045 13 pp. total Edinburgh, UK
A detailed treatment of the nominal algebra presented in our abstract in NWPT06. Subsumed by a journal version.
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.
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.
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.
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.
Logical Methods in Computer Science vol. 14, no. 2 article 12
Quine’s stratification condition viewed from the perspective of the theory of rewriting.
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〉”.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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
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.
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.
Second Workshop on Meta-Logic (MLG 2002) 2 pp. total Kinosaki, Japan
A prose account of my talk at MLG02 in Kinosaki, Japan.
University of Cambridge Cambridge, UK
See also the survey paper on foundations on nominal techniques.
Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS 1999) pp. 214–224 IEEE Computer Society Press
My first conference paper. See also the journal version.
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.
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
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’.
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.)
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.)
SIGPLAN Notices vol. 38 pp. 263–274 ACM Press
ML enriched with Gabbay-Pitts atoms-abstraction and nominal name-generation and pattern-matching.
Proceedings of the 5th international conference on the mathematics of program construction (MPC 2000) Lecture Notes in Computer Science vol. 1837 pp. 230–255 Springer
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
Logical Methods in Computer Science vol. 14, no. 2 article 12
Quine’s stratification condition viewed from the perspective of the theory of rewriting.
Electronic Notes in Theoretical Computer Science vol. 323 pp. 39–56 Elsevier B.V. ISSN 1571-0661
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.
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.
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.
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.
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
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.
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.
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.
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.
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.
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.
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.
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.
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.
Proceedings of LFMTP’06: First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice eds. Alberto Momigliano, Brigitte Pientka pp. 32–45 Seattle, Washington, USA
Proceedings of the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2005) pp. 47–58 ACM Press
We generalise and extend previous work on rewriting with variable binding, with name generation/restriction, and study its properties.
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.
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.
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.
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
Mathematical Structures in Computer Science vol. 36 article e3 Cambridge University Press
arXiv latest revision
Journal of Applied Logics vol. 12, no. 6 pp. 1481–1548 London: College Publications ISSN 2631-9810
Journal of Logic and Computation vol. 35, no. 5 article exae050 Oxford University Press online
Studies in Logic vol. 108 320 pp. total London: College Publications edition 1 ISBN 978-1-84890-465-1
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.
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.
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.
The IfCoLog Journal of Logics and their Applications vol. 1, no. 2 pp. 83–106 College Publications ISBN 978-1-84890-163-6 ISSN 2055-3706
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.
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.
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!
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.
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.
Subsumed by “Denotation of contextual modal type theory (CMTT): syntax and meta-programming”.
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.
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.
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.
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.
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.
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.
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.
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.
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
Mathematical Structures in Computer Science vol. 36 article e3 Cambridge University Press
arXiv latest revision
Journal of Logic and Computation vol. 35, no. 5 article exae050 Oxford University Press online
Studies in Logic vol. 108 320 pp. total London: College Publications edition 1 ISBN 978-1-84890-465-1
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.
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.
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
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
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
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
A revised and expanded exploration of a new and simple mathematical model of blockchains
Thanks to the Galois talk organisers. Video online here.
Galois Tech Talk series USA / online
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
An observation of nominal techniques is that names are a datatype
Thanks to the ICALP organisers. See the ICALP programme.
ICALP 2019 Patras, Greece
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
186 items, arranged by date.
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
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
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
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
I give an accessible introduction to my paper on Arithmetisation of computation via polynomial semantics for first-order logic in the Journal of Applied Logics, Volume 12, number 6, pp 1481–1548, October 2025.
Presented by Murdoch J. Gabbay Imperial College Research Seminar
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
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
A presentation of zkFOL (arithmetisation of first-order logic) to Circle’s cryptography group.
Presented by Murdoch J. Gabbay Circle Research Seminar
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
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
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
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
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
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
I discuss zkFOL, the arithmetisation of first-order logic validity over finite models.
Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2024 (SPLV24) University of Strathclyde Glasgow, Scotland
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
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
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
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
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
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
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
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.
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
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
An online presentation of my Cairo property-based and unit test suite (also on GitHub).
Thanks to Matchbox DAO for the kind invitation to speak.
Matchbox DAO Online
What it takes to implement a nominal package in a programming language, drawing on the Nominal Haskell package.
Presented by Murdoch J. Gabbay Scottish Programming Languages Seminar (SPLS) Hosted by University of Strathclyde Online
Introducing: a Nominal monad
Thanks to the Huawei-Edinburgh Joint Lab. Seminar details and video here.
Huawei–Edinburgh Joint Lab Edinburgh, UK
On the foundations of nominal techniques
Thanks to the summer school organisers.
XIII Summer Workshop in Mathematics Hosted by Universidade de Brasília Online
Consensus = Topology
Thanks to the Galois talk organisers. Video online here.
Galois Tech Talk series USA / online
Consensus = Topology Thanks to the FRIDA organisers.
7th Workshop on Formal Reasoning in Distributed Algorithms (FRIDA 2020) Online
A revised and expanded exploration of a new and simple mathematical model of blockchains
Thanks to the Galois talk organisers. Video online here.
Galois Tech Talk series USA / online
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
An exploration of a new and simple mathematical model of blockchains
Thanks to Ohad Kammar. See the LFCS Seminar series videos online.
LFCS seminar series, University of Edinburgh Edinburgh, UK / online
Outline of a nominal datatypes package.
Thanks to the summer school organisers. See the summer school webpage.
International Summer School on Metaprogramming 2019 Schloss Dagstuhl, Germany
An observation of nominal techniques is that names are a datatype
Thanks to the ICALP organisers. See the ICALP programme.
ICALP 2019 Patras, Greece
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
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
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
I visit the maths department.
Thanks to the Maximals seminar series.
Maximals seminar, Heriot-Watt University Edinburgh, UK
A seminar given to local MSc students, on technical writing.
MSc course, Heriot-Watt University Edinburgh, UK
Just a lovely, friendly event.
Thanks to the SPLS, and to the Departmental Seminar series of Strathclyde.
Scottish Programming Languages Seminar, University of Strathclyde Glasgow, UK
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
This was the second of two connected presentations; see next talk. Thanks to the Logic Colloquium, and to Nicola Gambino for being a gentleman.
Logic Colloquium 2016 Leeds, UK
What a nice event the Logic Colloquium was. What a treat to be surrounded by people who care so much about logic I learned a lot.
Thanks to the Logic Colloquium.
Logic Colloquium 2016 Leeds, UK
Thanks to the LFCS Seminars series.
LFCS seminar series, University of Edinburgh Edinburgh, UK
Thanks to the Birmingham Theory Seminars.
Birmingham Theory Seminar University of Birmingham, UK
Thanks to the Heriot-Watt Computer Science Seminar Series.
Computer Science Seminar, Heriot-Watt University Edinburgh, UK
Thanks to the King’s College London Informatics Research Colloquium Series.
Informatics Research Colloquium, King's College London London, UK
Thanks to the Manchester Logic Seminar series.
Manchester Logic Seminar, University of Manchester Manchester, UK
Thanks to the Logic and Semantics seminar series.
Logic and Semantics Seminar, University of Cambridge Cambridge, UK
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
Presented by Murdoch J. Gabbay Midlands Logic Seminar
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
See the announcement.
Thanks to the Leeds Logic Group.
Leeds Logic Group, University of Leeds Leeds, UK
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
Just as the title says!
Thanks to Neil Ghani and his lively and interesting group for the very enjoyable afternoon.
University of Strathclyde Glasgow, UK
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
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
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
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
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
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
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
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
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
Presentation at the 9th Italian Convention on Computational Logic (CILC’2012) in Rome, Italy. See also the associated paper, which is called Nominal semantics for predicate logic.
9th Italian Convention on Computational Logic (CILC 2012) Rome, Italy
Seminar at the School of Natural and Computing Sciences at the University of Aberdeen. I describe the nature of and motivation for nominal research.
School of Natural and Computing Sciences, University of Aberdeen Aberdeen, UK
Talk given at the mathematically structured programming group as part of the STP (Scottish Theorem Provers) meeting. I describe upcoming research to give a semantics to meta-variables in proof-search and theorem-proving.
Scottish Theorem Provers meeting, University of Strathclyde Glasgow, UK
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
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
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
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
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
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
Given at the Artificial Intelligence Research Institute (IIIA) in Barcelona, Spain. Does what it says on the tin. I gave the talk on the whiteboard; there are no slides.
Artificial Intelligence Research Institute (IIIA) Barcelona, Spain
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
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
A talk given at Glasgow University maths department. I discuss nominal techniques from a foundational point of view.
Mathematics Seminar, University of Glasgow Glasgow, UK
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
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
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
Part of the fun in the afternoon series of meetings. I describe current work with Dominic Mulligan on representing incompleteness in theorem-provers.
Thanks to Conor McBride.
Fun in the Afternoon meeting, University of Strathclyde Glasgow, UK
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
A talk given at the Typical Seminar at the École Polytechnique in Paris, France. I describe recent work on a representation theorem for the NEW-quantifier.
Thanks to Gilles Dowek and DIGITEO.
Typical Seminar, LIX, École Polytechnique Paris, France
Given at the 2010 British Logic Colloquium in Birmingham, UK. I describe in broad terms names and their symmetry properties.
Thanks to Eike Ritter.
British Logic Colloquium 2010 Birmingham, UK
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
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
Given as part of the Computer Science Seminars in Leicester, UK. I discuss permissive-nominal logic; an extension of first-order logic with names and binding.
Thanks to Alexander Kurz.
Computer Science Seminar, University of Leicester Leicester, UK
A talk given at the Scottish Theorem Proving meeting in Scotland, UK. I discuss permissive nominal terms. I used the whiteboard; there are no slides.
Thanks Grant Passmore.
Scottish Theorem Proving meeting, University of Edinburgh Edinburgh, UK
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
A 30 minute ‘theory lunch’ seminar given at IMDEA in Madrid, Spain. I discuss permissive nominal terms. I used the whiteboard; there are no slides.
Thanks to Alejandro Sanchez.
Theory Lunch, IMDEA Software Institute Madrid, Spain
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
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
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
I discuss technical writing for an audience of fourth year undergraduates, on Wednesday 22 October at 13:15. Oh, what are the laws of writing a good dissertation? Read the slides and find out, with examples!
Heriot-Watt University Edinburgh, UK
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
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
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
Talk given on Monday 30 June in the Pisa University Department of Informatics Seminar series in Italy at 17:30. I describe nominal algebra, a nominal algebraic reasoning language.
Department of Informatics Seminar, Università di Pisa Pisa, Italy
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
A talk given at the École Polytechnique on Tuesday 4 March at 11am. Joint work with Dominic Mulligan.
École Polytechnique / LIX Paris, France
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
A talk given in the DSG (Dependable Systems Group) meeting. Joint work with Dominic Mulligan.
Dependable Systems Group meeting, Heriot-Watt University Edinburgh, UK
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
A King’s College London departmental colloquium given on January 14 at noon. I gave this talk the old-fashioned way on the blackboard; hence, no pdf slides online. It was good fun.
Thanks to Iman Poernomo.
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
Given in the Prose seminar series at TU/e in Eindhoven on November 14 at 15:30. I talk about where I think things should be going.
Prose seminar series, Eindhoven University of Technology Eindhoven, Netherlands
Given at LFMTP, part of CADE07 near Bremen on July 15 at 17:00. Joint work with Stéphane Lengrand”.
Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), CADE 2007 Bremen, Germany
Workshop on Functional and Logic Programming, RDP 2007 Paris, France
A talk given at the LFCS logic and semantics club in Edinburgh University on June 15 at 13:00. Thanks to Bartek Klin.
Logic and Semantics Club, University of Edinburgh Edinburgh, UK
A talk given at Queen Mary and Westfield New College on June 4 at 15:30. Thanks to Hongseok Yang.
Queen Mary, University of London London, UK
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
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
I consider denotations for functional programming in substitution sets, an algebraic semantics for substitution.
Presented by Murdoch J. Gabbay DSG Digest, Heriot-Watt University Edinburgh, Scotland
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
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
A talk given at Heriot-Watt University on February 20 at 14:00. We discuss a recent paper in which I exhibit a substitution action on the Fraenkel-Mostowski sets universe. Thanks to Pierluigi Frisco.
Heriot-Watt University Edinburgh, UK
Given at St Andrew’s University on December 19 at 11:00. We discuss boxology and hierarchical nominal techniques. Thanks to Kevin Hammond.
University of St Andrews St Andrews, UK
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
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
A talk given at the University of Bath Computer Science Department on November 13 at 11:15. We discuss nominal logic and the slogans ‘logic with names’ versus ‘logic with variables’. Thanks to Mark Price and Alessio Guglielmi.
A talk given at the Dependable Systems Group weekly seminar at Heriot-Watt on October 27 at 14:15. We discuss what happens to the lambda binder in the presence of a hierarchy of variables.
Dependable Systems Group Seminar, Heriot-Watt University Edinburgh, UK
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
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
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
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
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
Presented at PPDP06 in Venice, Italy on Tuesday 11 July 2006 at 16:30.
Principles and Practice of Declarative Programming (PPDP 2006) Venice, Italy
Presented at the CANS seminar on Thursday 22 June 2006 at 3pm. Thanks to Maribel Fernández.
CANS Seminar, King's College London London, UK
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
Presented as part of a course in Tel-Aviv University at 12:00 on Sunday 28 May.
Presented by Murdoch J. Gabbay Mini-course Tel Aviv University Tel Aviv, Israel
Presented at the programming languages group in Tel-Aviv University at 14:00 on Sunday 28 May. Thanks to Mooly Sagiv.
Programming Languages Group, Tel Aviv University Tel Aviv, Israel
Presented as part of a course in Tel-Aviv University in 210 Schreiber at 12:00 on Sunday 14 May. Also see gabbay:newcc.
Presented by Murdoch J. Gabbay Mini-course Tel Aviv University Tel Aviv, Israel
Presented as part of a course in Tel-Aviv University in 210 Schreiber at 10:30 on Thursday 11 May. Also see gabbay:capasn and gabbay:subaan.
Presented by Murdoch J. Gabbay Mini-course Tel Aviv University Tel Aviv, Israel
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
Talk given at Tel-Aviv University on 6 October 2005. We give a non-technical account of Nominal Rewriting. Thanks to Arnon Avron and Nachum Dershowitz.
Tel Aviv University Tel Aviv, Israel
Talk given at Leicester University on 9 August 2005. We discuss Nominal Rewriting and suggest why it and the methods underlying it are of interest.
University of Leicester Leicester, UK
Talk given at LMU in Munich on 26 July 2005. We give a broad view of our research, mentioning a-logic and a whole load of other stuff.
LMU Munich Munich, Germany
Talk given at South Bank University in London on 25 July 2005. We discuss Restart, a Natural Deduction rule which turns intuitionistic logic into classical logic, without affecting proof-normalisation.
London South Bank University London, UK
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
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
Talk given at LIX, Ecole Polytechnique, France, on 24 May. Thanks to Dale Miller. 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.
LIX, École Polytechnique Paris, France
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
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
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
Slides of a talk given at the departmental colloquium on 24 November 2004.
Departmental Colloquium, King's College London London, UK
Slides of a talk given in Imperial College, London, on 10 September 2004. Thanks to Stephen Muggleton.
Imperial College London London, UK
Slides of a talk at PPDP04 on joint work with Maribel Fernández and Ian Mackie, given in Verona, Italy, on 26 August 2004. See also the paper.
Principles and Practice of Declarative Programming (PPDP 2004) Verona, Italy
Slides of a talk at LICS04 on joint work with James Cheney, given in Turku, Finland, on 15 July 2004. See also the paper.
Logic in Computer Science (LICS 2004) Turku, Finland
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
Talk given at PPS on 4 May 2004.
PPS Paris, France
We discuss extensions of Nominal Terms (see the paper on Nominal Unification). Lots of blue sky, but pretty.
Not recorded in the legacy archive
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
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
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
Talk given on Fresh Logic (a first-order logic for the NEW-quantifier with proof-normalisation) on 2 June at the local group’s weekly Semantics Lunch. See also an abstract.
Semantics Lunch, University of Cambridge Cambridge, UK
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
Talk given on May 28 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
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
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
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
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
Talk given in Pisa on 2/12/2002. Thanks to Ugo Montanari.
University of Pisa Pisa, Italy
Talk given in Cambridge on 11/11/2002 at the local group’s “Semantics Lunch”.
Semantics Lunch, University of Cambridge Cambridge, UK
Talk given at the Max-Planck Institute, Saarbrücken, Germany.
Max Planck Institute Saarbrücken, Germany
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
Talk given at IBM Research, Haifa, Israel 2/10/02. Thanks to Cindy Eisner.
IBM Research Haifa, Israel
Contributed talk at Workshop on Thirty Five years of Automath, Informal Proceedings, Heriot-Watt University, Edinburgh, Scotland, April 2002.
Workshop on Thirty Five Years of Automath Heriot-Watt University, Edinburgh, UK
Some talks appear under more than one topic.
I visit the maths department.
Thanks to the Maximals seminar series.
Maximals seminar, Heriot-Watt University Edinburgh, UK
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
Talk given on Monday 30 June in the Pisa University Department of Informatics Seminar series in Italy at 17:30. I describe nominal algebra, a nominal algebraic reasoning language.
Department of Informatics Seminar, Università di Pisa Pisa, Italy
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
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
Presented at the CANS seminar on Thursday 22 June 2006 at 3pm. Thanks to Maribel Fernández.
CANS Seminar, King's College London London, UK
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
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
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
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
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
A revised and expanded exploration of a new and simple mathematical model of blockchains
Thanks to the Galois talk organisers. Video online here.
Galois Tech Talk series USA / online
An exploration of a new and simple mathematical model of blockchains
Thanks to Ohad Kammar. See the LFCS Seminar series videos online.
LFCS seminar series, University of Edinburgh Edinburgh, UK / online
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
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
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
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
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
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
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
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
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
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
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
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
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
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.
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
Consensus = Topology
Thanks to the Galois talk organisers. Video online here.
Galois Tech Talk series USA / online
Consensus = Topology Thanks to the FRIDA organisers.
7th Workshop on Formal Reasoning in Distributed Algorithms (FRIDA 2020) Online
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
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
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
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
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
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
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
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
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
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
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
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
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
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
A talk given in the DSG (Dependable Systems Group) meeting. Joint work with Dominic Mulligan.
Dependable Systems Group meeting, Heriot-Watt University Edinburgh, UK
Given at LFMTP, part of CADE07 near Bremen on July 15 at 17:00. Joint work with Stéphane Lengrand”.
Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), CADE 2007 Bremen, Germany
Given at St Andrew’s University on December 19 at 11:00. We discuss boxology and hierarchical nominal techniques. Thanks to Kevin Hammond.
University of St Andrews St Andrews, UK
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
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
Presented as part of a course in Tel-Aviv University in 210 Schreiber at 12:00 on Sunday 14 May. Also see gabbay:newcc.
Presented by Murdoch J. Gabbay Mini-course Tel Aviv University Tel Aviv, Israel
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
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
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
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
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
I give an accessible introduction to my paper on Arithmetisation of computation via polynomial semantics for first-order logic in the Journal of Applied Logics, Volume 12, number 6, pp 1481–1548, October 2025.
Presented by Murdoch J. Gabbay Imperial College Research Seminar
A presentation of zkFOL (arithmetisation of first-order logic) to Circle’s cryptography group.
Presented by Murdoch J. Gabbay Circle Research Seminar
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
I discuss zkFOL, the arithmetisation of first-order logic validity over finite models.
Presented by Murdoch J. Gabbay Scottish Programming Languages and Verification Summer School 2024 (SPLV24) University of Strathclyde Glasgow, Scotland
What a nice event the Logic Colloquium was. What a treat to be surrounded by people who care so much about logic I learned a lot.
Thanks to the Logic Colloquium.
Logic Colloquium 2016 Leeds, UK
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
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
Presentation at the 9th Italian Convention on Computational Logic (CILC’2012) in Rome, Italy. See also the associated paper, which is called Nominal semantics for predicate logic.
9th Italian Convention on Computational Logic (CILC 2012) Rome, Italy
Talk given at the mathematically structured programming group as part of the STP (Scottish Theorem Provers) meeting. I describe upcoming research to give a semantics to meta-variables in proof-search and theorem-proving.
Scottish Theorem Provers meeting, University of Strathclyde Glasgow, UK
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
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
Part of the fun in the afternoon series of meetings. I describe current work with Dominic Mulligan on representing incompleteness in theorem-provers.
Thanks to Conor McBride.
Fun in the Afternoon meeting, University of Strathclyde Glasgow, UK
Given at the 2010 British Logic Colloquium in Birmingham, UK. I describe in broad terms names and their symmetry properties.
Thanks to Eike Ritter.
British Logic Colloquium 2010 Birmingham, UK
Given as part of the Computer Science Seminars in Leicester, UK. I discuss permissive-nominal logic; an extension of first-order logic with names and binding.
Thanks to Alexander Kurz.
Computer Science Seminar, University of Leicester Leicester, UK
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
A talk given at the École Polytechnique on Tuesday 4 March at 11am. Joint work with Dominic Mulligan.
École Polytechnique / LIX Paris, France
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
Workshop on Functional and Logic Programming, RDP 2007 Paris, France
A talk given at the LFCS logic and semantics club in Edinburgh University on June 15 at 13:00. Thanks to Bartek Klin.
Logic and Semantics Club, University of Edinburgh Edinburgh, UK
A talk given at Queen Mary and Westfield New College on June 4 at 15:30. Thanks to Hongseok Yang.
Queen Mary, University of London London, UK
A talk given at the University of Bath Computer Science Department on November 13 at 11:15. We discuss nominal logic and the slogans ‘logic with names’ versus ‘logic with variables’. Thanks to Mark Price and Alessio Guglielmi.
A talk given at the Dependable Systems Group weekly seminar at Heriot-Watt on October 27 at 14:15. We discuss what happens to the lambda binder in the presence of a hierarchy of variables.
Dependable Systems Group Seminar, Heriot-Watt University Edinburgh, UK
Presented at PPDP06 in Venice, Italy on Tuesday 11 July 2006 at 16:30.
Principles and Practice of Declarative Programming (PPDP 2006) Venice, Italy
Presented at the programming languages group in Tel-Aviv University at 14:00 on Sunday 28 May. Thanks to Mooly Sagiv.
Programming Languages Group, Tel Aviv University Tel Aviv, Israel
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
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
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
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
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
Talk given at LMU in Munich on 26 July 2005. We give a broad view of our research, mentioning a-logic and a whole load of other stuff.
LMU Munich Munich, Germany
Talk given at South Bank University in London on 25 July 2005. We discuss Restart, a Natural Deduction rule which turns intuitionistic logic into classical logic, without affecting proof-normalisation.
London South Bank University London, UK
Slides of a talk given at the departmental colloquium on 24 November 2004.
Departmental Colloquium, King's College London London, UK
Slides of a talk at LICS04 on joint work with James Cheney, given in Turku, Finland, on 15 July 2004. See also the paper.
Logic in Computer Science (LICS 2004) Turku, Finland
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
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
Talk given on Fresh Logic (a first-order logic for the NEW-quantifier with proof-normalisation) on 2 June at the local group’s weekly Semantics Lunch. See also an abstract.
Semantics Lunch, University of Cambridge Cambridge, UK
Contributed talk at Workshop on Thirty Five years of Automath, Informal Proceedings, Heriot-Watt University, Edinburgh, Scotland, April 2002.
Workshop on Thirty Five Years of Automath Heriot-Watt University, Edinburgh, UK
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
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
What it takes to implement a nominal package in a programming language, drawing on the Nominal Haskell package.
Presented by Murdoch J. Gabbay Scottish Programming Languages Seminar (SPLS) Hosted by University of Strathclyde Online
Introducing: a Nominal monad
Thanks to the Huawei-Edinburgh Joint Lab. Seminar details and video here.
Huawei–Edinburgh Joint Lab Edinburgh, UK
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
Outline of a nominal datatypes package.
Thanks to the summer school organisers. See the summer school webpage.
International Summer School on Metaprogramming 2019 Schloss Dagstuhl, Germany
An observation of nominal techniques is that names are a datatype
Thanks to the ICALP organisers. See the ICALP programme.
ICALP 2019 Patras, Greece
Thanks to the Birmingham Theory Seminars.
Birmingham Theory Seminar University of Birmingham, UK
Just as the title says!
Thanks to Neil Ghani and his lively and interesting group for the very enjoyable afternoon.
University of Strathclyde Glasgow, UK
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
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
Given at the Artificial Intelligence Research Institute (IIIA) in Barcelona, Spain. Does what it says on the tin. I gave the talk on the whiteboard; there are no slides.
Artificial Intelligence Research Institute (IIIA) Barcelona, Spain
A talk given at Glasgow University maths department. I discuss nominal techniques from a foundational point of view.
Mathematics Seminar, University of Glasgow Glasgow, UK
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
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
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
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
A talk given at the Typical Seminar at the École Polytechnique in Paris, France. I describe recent work on a representation theorem for the NEW-quantifier.
Thanks to Gilles Dowek and DIGITEO.
Typical Seminar, LIX, École Polytechnique Paris, France
A talk given at the Scottish Theorem Proving meeting in Scotland, UK. I discuss permissive nominal terms. I used the whiteboard; there are no slides.
Thanks Grant Passmore.
Scottish Theorem Proving meeting, University of Edinburgh Edinburgh, UK
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
A 30 minute ‘theory lunch’ seminar given at IMDEA in Madrid, Spain. I discuss permissive nominal terms. I used the whiteboard; there are no slides.
Thanks to Alejandro Sanchez.
Theory Lunch, IMDEA Software Institute Madrid, Spain
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
Given in the Prose seminar series at TU/e in Eindhoven on November 14 at 15:30. I talk about where I think things should be going.
Prose seminar series, Eindhoven University of Technology Eindhoven, Netherlands
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
I consider denotations for functional programming in substitution sets, an algebraic semantics for substitution.
Presented by Murdoch J. Gabbay DSG Digest, Heriot-Watt University Edinburgh, Scotland
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
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
A talk given at Heriot-Watt University on February 20 at 14:00. We discuss a recent paper in which I exhibit a substitution action on the Fraenkel-Mostowski sets universe. Thanks to Pierluigi Frisco.
Heriot-Watt University Edinburgh, UK
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
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
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
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
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
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
Talk given at PPS on 4 May 2004.
PPS Paris, France
We discuss extensions of Nominal Terms (see the paper on Nominal Unification). Lots of blue sky, but pretty.
Not recorded in the legacy archive
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
Talk given at the Max-Planck Institute, Saarbrücken, Germany.
Max Planck Institute Saarbrücken, Germany
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
Talk given at IBM Research, Haifa, Israel 2/10/02. Thanks to Cindy Eisner.
IBM Research Haifa, Israel
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
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
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
Talk given in Pisa on 2/12/2002. Thanks to Ugo Montanari.
University of Pisa Pisa, Italy
Talk given in Cambridge on 11/11/2002 at the local group’s “Semantics Lunch”.
Semantics Lunch, University of Cambridge Cambridge, UK
An online presentation of my Cairo property-based and unit test suite (also on GitHub).
Thanks to Matchbox DAO for the kind invitation to speak.
Matchbox DAO Online
Talk given on May 28 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
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
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
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
Presented as part of a course in Tel-Aviv University in 210 Schreiber at 10:30 on Thursday 11 May. Also see gabbay:capasn and gabbay:subaan.
Presented by Murdoch J. Gabbay Mini-course Tel Aviv University Tel Aviv, Israel
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
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
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
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
Talk given at Tel-Aviv University on 6 October 2005. We give a non-technical account of Nominal Rewriting. Thanks to Arnon Avron and Nachum Dershowitz.
Tel Aviv University Tel Aviv, Israel
Talk given at Leicester University on 9 August 2005. We discuss Nominal Rewriting and suggest why it and the methods underlying it are of interest.
University of Leicester Leicester, UK
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
Talk given at LIX, Ecole Polytechnique, France, on 24 May. Thanks to Dale Miller. 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.
LIX, École Polytechnique Paris, France
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
Slides of a talk given in Imperial College, London, on 10 September 2004. Thanks to Stephen Muggleton.
Imperial College London London, UK
Slides of a talk at PPDP04 on joint work with Maribel Fernández and Ian Mackie, given in Verona, Italy, on 26 August 2004. See also the paper.
Principles and Practice of Declarative Programming (PPDP 2004) Verona, Italy
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
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
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
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
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
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
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
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
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
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
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
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
A King’s College London departmental colloquium given on January 14 at noon. I gave this talk the old-fashioned way on the blackboard; hence, no pdf slides online. It was good fun.
Thanks to Iman Poernomo.
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
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
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
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
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
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
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.
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
Consensus = Topology
Thanks to the Galois talk organisers. Video online here.
Galois Tech Talk series USA / online
Consensus = Topology Thanks to the FRIDA organisers.
7th Workshop on Formal Reasoning in Distributed Algorithms (FRIDA 2020) Online
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
On the foundations of nominal techniques
Thanks to the summer school organisers.
XIII Summer Workshop in Mathematics Hosted by Universidade de Brasília Online
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
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
Just a lovely, friendly event.
Thanks to the SPLS, and to the Departmental Seminar series of Strathclyde.
Scottish Programming Languages Seminar, University of Strathclyde Glasgow, UK
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
This was the second of two connected presentations; see next talk. Thanks to the Logic Colloquium, and to Nicola Gambino for being a gentleman.
Logic Colloquium 2016 Leeds, UK
Thanks to the LFCS Seminars series.
LFCS seminar series, University of Edinburgh Edinburgh, UK
Thanks to the Heriot-Watt Computer Science Seminar Series.
Computer Science Seminar, Heriot-Watt University Edinburgh, UK
Thanks to the King’s College London Informatics Research Colloquium Series.
Informatics Research Colloquium, King's College London London, UK
Thanks to the Manchester Logic Seminar series.
Manchester Logic Seminar, University of Manchester Manchester, UK
Thanks to the Logic and Semantics seminar series.
Logic and Semantics Seminar, University of Cambridge Cambridge, UK
Presented by Murdoch J. Gabbay Midlands Logic Seminar
See the announcement.
Thanks to the Leeds Logic Group.
Leeds Logic Group, University of Leeds Leeds, UK
Seminar at the School of Natural and Computing Sciences at the University of Aberdeen. I describe the nature of and motivation for nominal research.
School of Natural and Computing Sciences, University of Aberdeen Aberdeen, UK
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
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
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
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
Presented as part of a course in Tel-Aviv University at 12:00 on Sunday 28 May.
Presented by Murdoch J. Gabbay Mini-course Tel Aviv University Tel Aviv, Israel
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
A seminar given to local MSc students, on technical writing.
MSc course, Heriot-Watt University Edinburgh, UK
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
I discuss technical writing for an audience of fourth year undergraduates, on Wednesday 22 October at 13:15. Oh, what are the laws of writing a good dissertation? Read the slides and find out, with examples!
Heriot-Watt University Edinburgh, UK
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
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
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
I hope you find the following software interesting and perhaps informative. I enjoyed writing it.
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.
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.
A model checker for 3muQL, for checking whether a model satisfies specified logical properties. See the related Declarative Paxos paper.
An efficient implementation of the Arithmetisation of first-order logic paper, with thanks to Andrew Mendelsohn and Jeremy Ornelas.
Names, swapping, binding, and capture-avoiding programming, with examples for the lambda-calculus, System F, and EUTxO.
See also the August 2020 SPLV notes and recordings
Archived Cairo 0.x tools from the earlier Python ecosystem: bitwise integers over field elements and property-based testing.
Small programs written when I remember that computers are supposed to save labour.
“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
Recognised in
The Coinspondent · Friedemann Brenneis
“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.
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)
Recognised in
ACM SIGLOG · EATCS · EACSL · Kurt Gödel Society
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.
Murdoch J. Gabbay and Andrew M. Pitts · Formal Aspects of Computing 13(3–5), 341–363 (2002)
Andrew M. Pitts · Information and Computation 186(2), 165–193 (2003)
Recognised in
ACM/IEEE Symposium on Logic in Computer Science
Recipients Murdoch J. Gabbay and Andrew M. Pitts
Recognised twenty years after LICS 1999 for its lasting influence.
Murdoch J. Gabbay and Andrew M. Pitts · Proceedings of LICS 1999, 214–224
Recognised in
Principles and Practice of Declarative Programming
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.
Maribel Fernández, Murdoch J. Gabbay, and Ian Mackie · Proceedings of PPDP 2004, 108–119
If you cite my work, please use Murdoch J. Gabbay rather than M. J. Gabbay: my brother Mike has the same initials.
The Journal of Financial Technology is free and open-access, bringing together mathematics, statistics, computer science, finance, and law in fintech.
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 usually just ask for the "gluten-free"
option.
It's a simplification, but a useful one in practice.
For your convenience, my homepage is available in Swedish Chef (see Wikipedia and YouTube).
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.