142 citations · 346 across the 11 of their papers we have counts for
15 papers
Propositional Logics for the Lawvere Quantale
Giorgio Bacci, Radu Mardare, Prakash Panangaden +1
Lawvere showed that generalised metric spaces are categories enriched over , the quantale of the positive extended reals. The statement of enrichment is a quantitative…
Sum and Tensor of Quantitative Effects
Giorgio Bacci, Radu Mardare, Prakash Panangaden +1
Inspired by the seminal work of Hyland, Plotkin, and Power on the combination of algebraic computational effects via sum and tensor, we develop an analogous theory for the combinat…
Recursion does not always help
Gordon Plotkin
We show that adding recursion does not increase the total functions definable in the typed -calculus or the partial functions definable in the -calculus. As a consequence,…
Fixed-Points for Quantitative Equational Logics
Radu Mardare, Prakash Panangaden, Gordon Plotkin
We develop a fixed-point extension of quantitative equational logic and give semantics in one-bounded complete quantitative algebras. Unlike previous related work about fixed-point…
Smart Choices and the Selection Monad
Martin Abadi, Gordon Plotkin
Describing systems in terms of choices and their resulting costs and rewards offers the promise of freeing algorithm designers and programmers from specifying how those choices sho…
A complete equational axiomatisation of partial differentiation
Gordon D. Plotkin
We formalise the well-known rules of partial differentiation in a version of equational logic with function variables and binding constructs. We prove the resulting theory is compl…
A Simple Differentiable Programming Language
Martin Abadi, Gordon D. Plotkin
Automatic differentiation plays a prominent role in scientific computing and in modern machine learning, often in the context of powerful programming systems. The relation of the v…
Reverse derivative categories
Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher +4
The reverse derivative is a fundamental operation in machine learning and automatic differentiation. This paper gives a direct axiomatization of a category with a reverse derivativ…
On the Axiomatizability of Quantitative Algebras
Radu Mardare, Prakash Panangaden, Gordon Plotkin
Quantitative algebras (QAs) are algebras over metric spaces defined by quantitative equational theories as introduced by the same authors in a related paper presented at LICS 2016.…
Free complete Wasserstein algebras
Radu Mardare, Prakash Panangaden, Gordon D. Plotkin
We present an algebraic account of the Wasserstein distances on complete metric spaces, for . This is part of a program of a quantitative algebraic theory of effect…
Mixed powerdomains for probability and nondeterminism
Klaus Keimel, Gordon D. Plotkin
We consider mixed powerdomains combining ordinary nondeterminism and probabilistic nondeterminism. We characterise them as free algebras for suitable (in)equation-al theories; we e…
Dijkstra Monads for Free
Danel Ahman, Catalin Hritcu, Kenji Maillard +5
Dijkstra monads enable a dependent type theory to be enhanced with support for specifying and verifying effectful code via weakest preconditions. Together with their closely relate…
Handling Algebraic Effects
Gordon D Plotkin, Matija Pretnar
Algebraic effects are computational effects that can be represented by an equational theory whose operations produce the effects at hand. The free model of this theory induces the…
On CSP and the Algebraic Theory of Effects
Rob van Glabbeek, Gordon Plotkin
We consider CSP from the point of view of the algebraic theory of effects, which classifies operations as effect constructors or effect deconstructors; it also provides a link with…
Configuration Structures, Event Structures and Petri Nets
R. J. van Glabbeek, G. D. Plotkin
In this paper the correspondence between safe Petri nets and event structures, due to Nielsen, Plotkin and Winskel, is extended to arbitrary nets without self-loops, under the coll…