Gordon D. Plotkin

CSL Conference 2026 Conference Paper

Rational Lawvere Logic (Invited Paper)

• Giorgio Bacci
• Radu Mardare
• Prakash Panangaden
• Gordon D. Plotkin

We study Rational Lawvere logic (RL). This logic is defined over the extended positive reals with an algebraic structure combining the Lawvere quantale (with the reversed order on the extended reals and a sum as tensor) and a multiplicative quantale (with the usual order on the extended reals and a multiplication as tensor); together they provide a semiring structure. The logic is designed for complex quantitative reasoning, including sequents expressing inequalities between rational functions over the extended positive reals. We give a deduction system and demonstrate its expressiveness by deriving a classical result from probability theory relating the Kantorovich and total variation distances. Our deductive system is complete for finitely axiomatizable theories. The proof of completeness relies on the Krivine-Stengle Positivstellensatz. We additionally provide complexity results for both RL and its affine fragment AL. We consider two decision problems: the satisfiability of a set of sequents and whether a sequent follows from a finite set of sequent. We show that both problems lie in PSPACE for RL, and we give sharper complexity bounds for AL: the first problem is NP-complete, while the second is co-NP-complete.

CSL Conference 2020 Conference Paper

Reverse Derivative Categories

• J. Robin B. Cockett
• Geoff S. H. Cruttwell
• Jonathan Gallagher
• Jean-Simon Pacaud Lemay
• Benjamin MacAdam
• Gordon D. Plotkin
• Dorette Pronk

The reverse derivative is a fundamental operation in machine learning and automatic differentiation [Martín Abadi et al. , 2015; Griewank, 2012]. This paper gives a direct axiomatization of a category with a reverse derivative operation, in a similar style to that given by [Blute et al. , 2009] for a forward derivative. Intriguingly, a category with a reverse derivative also has a forward derivative, but the converse is not true. In fact, we show explicitly what a forward derivative is missing: a reverse derivative is equivalent to a forward derivative with a dagger structure on its subcategory of linear maps. Furthermore, we show that these linear maps form an additively enriched category with dagger biproducts.

TCS Journal 2019 Journal Article

Chromar, a language of parameterised agents

• Ricardo Honorato-Zimmer
• Andrew J. Millar
• Gordon D. Plotkin
• Argyris Zardilis

Modelling in biology becomes necessary when systems are complex. However, the more complex the systems are, the harder models become to read and write. The most common ways of writing models are by writing reactions on species (discrete objects), or by writing rate equations for the populations of such species. One problem with such approaches is that the number of species is often so large that the model cannot be realistically enumerated. Another problem is that the number of species and reactions often fixed by default, whereas new variations of species and reactions are constantly being improvised by evolution in the long-term and moment to moment by the changing chemical environments and compartments living organisms inhabit and create within. Here we develop a modelling language Chromar that provides an extension to the representation of reactions, in which objects, called agents, carry attributes with associated types — for example, Leaf agents all have a mass attribute. Dynamics are given by stochastic rules defined on groups of agents — for example all agents of a specific type — and so enumerating the dynamics of each agent is not necessary. This compact representation addresses the first problem. Having a more compact representation can also help make models a tool for knowledge representation and exchange instead of just simulation. Further, if we think of agents as the analogue of species in reactions, then creating a new agent of some type effectively creates a new species, thereby addressing the second problem. We then develop an extension of Chromar equipped with deterministically changing time-dependent values (fluents) and aggregate values computed from the state of the system (observables). Fluents are useful for describing the context of the system, which is rarely static; observables are useful in abstracting away details of system behaviour and providing a way to observe the system during simulation. Finally, we develop an embedding of Chromar (and its extensions) in the programming language Haskell and demonstrate its applicability via two examples. Embedding Chromar in a general purpose programming language such as Haskell eases some of the constraints of modelling languages while still maintaining the naturalness of a domain-specific language.

TCS Journal 2014 Journal Article

Cartesian closed categories of separable Scott domains

• Andrej Bauer
• Gordon D. Plotkin
• Dana S. Scott

We classify all sub-cartesian closed categories of the category of separable Scott domains. The classification employs a notion of coherence degree determined by the possible inconsistency patterns of sets of finite elements of a domain. Using the classification, we determine all sub-cartesian closed categories of the category of separable Scott domains that contain a universal object. The separable Scott domain models of the λβ-calculus are then classified up to a retraction by their coherence degrees.

MFCS Conference 2004 Conference Paper

Event Structures for Resolvable Conflict

• Rob J. van Glabbeek
• Gordon D. Plotkin

Abstract We propose a generalisation of Winskel’s event structures, matching the expressive power of arbitrary Petri nets. In particular, our event structures capture resolvable conflict, besides disjunctive and conjunctive causality.

CSL Conference 1998 Conference Paper

From Action Calculi to Linear Logic

• Andrew G. Barber
• Philippa Gardner
• Masahito Hasegawa
• Gordon D. Plotkin

Abstract Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the propositions-as-types paradigm; the type theory has a sound and complete interpretation in Power's categorical models. We go on to give a sound translation of our type theory in the (type theory of) intuitionistic linear logic, corresponding to the relation between Benton's models of linear logic and models of action calculi. The conservativity of the syntactic translation is proved by a model-embedding construction using the Yoneda lemma. Finally, we briefly discuss how these techniques can also be used to give conservative translations between various extensions of action calculi.

CSL Conference 1997 Conference Paper

An Extension of Models of Axiomatic Domain Theory to Models of Synthetic Domain Theory

• Marcelo P. Fiore
• Gordon D. Plotkin

Abstract We relate certain models of Axiomatic Domain Theory (ADT) and Synthetic Domain Theory (SDT). On the one hand, we introduce a class of non-elementary models of SDT and show that the domains in them yield models of ADT. On the other hand, for each model of ADT in a wide class we construct a model of SDT such that the domains in it provide a model of ADT which conservatively extends the original model.

TCS Journal 1993 Journal Article

A logical view of composition

• Martín Abadi
• Gordon D. Plotkin

We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification approaches; one of the logics is intuitionistic, while the other one is linear.

TCS Journal 1993 Journal Article

Set-theoretical and other elementary models of the λ-calculus

• Gordon D. Plotkin

Part I (pp. 351–373) of this paper is the previously unpublished 1972 memorandum (Plotkin, 1972) with editorial changes and some minor corrections. Part II (pp. 373–409) presents what happened next, together with some further development of the material. The first part begins with an elementary set-theoretical model of the λβ-calculus. Functions are modelled in a similar way to that normally employed in set theory, by their graphs; difficulties are caused in this enterprise by the axiom of foundation. Next, based on that model, a model of the λβη-calculus is constructed by means of a natural deduction method. Finally, a theorem is proved giving some general properties of those nontrivial models of the λβη-calculus which are continuous complete lattices. The second part begins with a brief discussion of models of the λ-calculus in set theories with anti-foundation axioms. Next the model of the λβ-calculus of Part I and also the closely related — but different! — models of Scott (1976, 1980) and of Engeler (1981, 1988) are reviewed. Then general frameworks in which elementary constructions of models can be given are discussed. Following Longo (1982), one can employ certain Scott-Engeler algebras. Following Coppo et al. (1983), one can obtain filter models from their extended applicative type structures. An extended discussion is given of various ways of constructing models of the λβη-calculus, and the connections between them. Finally an extension of the theorem to complete partial orders is given. The theme of the paper is the consideration of means of constructing models. There is hardly any analysis of their properties; there is no discussion of their application.

TARK Conference 1986 Conference Paper

A Framework for Intuitionistic Modal Logics

• Gordon D. Plotkin
• Colin Stirling

MFCS Conference 1980 Conference Paper

A Term Model for CCS

• Matthew Hennessy
• Gordon D. Plotkin

MFCS Conference 1979 Invited Paper

Full Abstraction for a Simple Parallel Programming Language

• Matthew Hennessy
• Gordon D. Plotkin

FOCS Conference 1977 Conference Paper

The Category-Theoretic Solution of Recursive Domain Equations (Extended Abstract)

• Michael B. Smyth
• Gordon D. Plotkin