35 citations · 124 across the 25 of their papers we have counts for
25 papers
Cryptographic certificates of validity for trustworthy AI
Murdoch J. Gabbay
We propose cryptographic certificates of validity for agentic AI systems. The core idea is to formally specify a correctness or policy condition as a logical predicate, compile thi…
Nominal techniques as an Agda library
Murdoch J. Gabbay, Orestis Melkonian
Nominal techniques provide a mathematically principled approach to dealing with names and variable binding in programming languages. This paper explores an attempt to make nominal…
Declarative distributed algorithms as axiomatic theories in three-valued modal logic over semitopologies
Murdoch J. Gabbay
We illustrate how to formally specify distributed algorithms as declarative axiomatic theories in a modal logic, using as illustrative examples a simple voting protocol, a simple b…
Decentralised collaborative action: cryptoeconomics in space
Murdoch J. Gabbay
Blockchains and peer-to-peer systems are part of a trend towards computer systems that are "radically decentralised", by which we mean that they 1) run across many participants, 2)…
A declarative approach to specifying distributed algorithms using three-valued modal logic
Murdoch J. Gabbay, Luca Zanolini
We present Coalition Logic, a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus alg…
Semitopology: distributed collaborative action via topology, algebra, and logic
Murdoch J. Gabbay
We introduce semitopologies, a generalisation of point-set topology that removes the restriction that intersections of open sets need necessarily be open. The intuition is that poi…
Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits
Gilles Dowek, Murdoch J. Gabbay
We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable…
Permissive-Nominal Logic (journal version)
Gilles Dowek, Murdoch J. Gabbay
Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments. This allows for direct axiomatisations with b…
Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
Gilles Dowek, Murdoch J. Gabbay, Dominic Mulligan
Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of 'freshness assumptions…
Semiframes: the algebra of semitopologies and actionable coalitions
Murdoch J. Gabbay
We introduce semiframes (an algebraic structure) and investigate their duality with semitopologies (a topological one). Both semitopologies and semiframes are relatively recent dev…
Semitopology: a topological approach to decentralised collaborative action
Murdoch Gabbay
We introduce semitopology, a generalisation of point-set topology that removes the restriction that intersections of open sets need necessarily be open. The intuition is that point…
Money grows on (proof-)trees: the formal FA1.2 ledger standard
Murdoch Gabbay, Arvid Jakobsson, Kristina Sojakova
Once you have invented digital money, you may need a ledger to track who owns what -- and an interface to that ledger so that users of your money can transact. On the Tezos blockch…
Karl Marx and the Blockchain
Devraj Basu, Murdoch Gabbay
Blockchain is often presented as a technological development; however, clearly it is not only that: the `Blockchain buzz' exists in the context of current social and political deve…
Algebras of UTxO blockchains
Murdoch J. Gabbay
We condense the theory of blockchains down to a simple and compact set of four type equations (Idealised EUTxO), and to an algebraic characterisation (abstract chunk systems), and…
UTxO- vs account-based smart contract blockchain programming paradigms
Lars Brunjes, Murdoch J. Gabbay
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 annotate…
Equivariant ZFA with Choice: a position paper
Murdoch J. Gabbay
We propose Equivariant ZFA with Choice as a foundation for nominal techniques that is stronger than ZFC and weaker than FM, and why this may be particularly helpful in the context…
Equivariant ZFA and the foundations of nominal techniques
Murdoch J. Gabbay
We give an accessible presentation to the foundations of nominal techniques, lying between Zermelo-Fraenkel set theory and Fraenkel-Mostowski set theory, and which has several nice…
The language of Stratified Sets is confluent and strongly normalising
Murdoch J. Gabbay
We study the properties of the language of Stratified Sets (first-order logic with and a stratification condition) as used in TST, TZT, and (with stratifiability instead of s…
Consistency of Quine's New Foundations
Murdoch J. Gabbay
We provide an elementary consistency proof of Quine's New Foundations, by a construction using interated nominal powersets.
Semantics out of context: nominal absolute denotations for first-order logic and computation
Murdoch J. Gabbay
Call a semantics for a language with variables absolute when variables map to fixed entities in the denotation. That is, a semantics is absolute when the denotation of a variable a…
Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness
Murdoch J. Gabbay, Michael J. Gabbay
We give a semantics for the lambda-calculus based on a topological duality theorem in nominal sets. A novel interpretation of lambda is given in terms of adjoints, and lambda-terms…
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
Murdoch Gabbay, Aleksandar Nanevski
The modal logic S4 can be used via a Curry-Howard style correspondence to obtain a lambda-calculus. Modal (boxed) types are intuitively interpreted as `closed syntax of the calculu…
Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
Murdoch J. Gabbay
By operations on models we show how to relate completeness with respect to permissive-nominal models to completeness with respect to nominal models with finite support. Models with…
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
Murdoch J. Gabbay, Dominic P. Mulligan
We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps t…