Papers

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.

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

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.

A new take on the foundations of nominal techniques.

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

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

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.

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.

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

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

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

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.

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

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

Stone duality for first-order logic. 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.

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

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.

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.

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.

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

The lambda-context calculus 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.

We can write axioms for the lambda-calculus in nominal algebra—but do we know those axioms are right? We prove completeness of axioms for alpha-beta-(eta) equivalence. This subsumes a previous book chapter.

Nominal 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

• Capture-avoiding substitution as a nominal algebra,
• One-and-a-halfth order logic,
• Nominal algebra and the HSP theorem, and
• A nominal axiomatisation of the lambda-calculus.

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.

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

We use nominal algebra to give a sound and complete axiomatisation of the lambda-calculus. Subsumed by a journal version.

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.

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

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

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.

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

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.

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.

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.

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.

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.

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.

We relate nominal algebra and rewriting, with concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality, which includes specifications of lambda-calculus and first-order logic.

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

We translate between equality derivations in lambda-theories and equality derivations in permissive-nominal algebra theories. This connects reasoning over higher-order syntax to reasoning over nominal terms.

Permissive nominal terms resemble nominal terms, but using infinite and co-infinite sets of atoms. We get ‘always fresh’ and ‘always alpha-rename’ properties familiar from first-and higher- order syntax but absent from nominal terms. See also the journal version

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

Nominal terms give Curry-Howard for schematic derivations. Atoms correspond with assumptions, unknowns correspond with schematic parts of the derivation, freshness conditions corresponds with the condition that an assumption will be discharged (even if the schema does not specify how).

Nominal renaming sets 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.

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.

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.

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

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.

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.

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.

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.

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.

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

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.

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

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

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

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

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

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.

My first conference paper. See also the journal version.

Subsumed by this journal paper.

Subsumed by this journal paper.

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.

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.

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.

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.

Subsumed by a journal paper. We prove the HSP (Homomorphism, Subalgebra, Product) theorem for Nominal Algebra, also known as Birkhoffs theorem.

Subsumed by a journal paper. Decidability and theory of models of a nominal algebra axiomatisation of capture-avoiding substitution.

A detailed treatment of the nominal algebra presented in "our abstract in NWPT06":#noma-nwpt. Subsumed by "a journal version":#noma-jv.

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

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

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

A photo of Michael delivering the talk.

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.

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

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

See also the survey paper on foundations on nominal techniques.