8 papers
On Models of the Planar Lambda Calculus
Chad Nester
We construct an adjunction relating two approaches to modelling the planar lambda calculus: semi-closed operads and planar lambda-models. We use this to obtain a planar version of…
Override and Update in Restriction Categories
Jean-Simon Pacaud Lemay, Chad Nester
We study the override and update operators on partial functions from the perspective of restriction categories. We propose a definition of override restriction categories, in which…
A Simple Categorical Calculus of Interacting Processes
Chad Nester, Niels Voorneveld
We present a calculus that models a simple sort of process interaction. Our calculus consists of a collection of terms together with a rewrite relation, parameterised by an arbitra…
Monoidal categories graded by partial commutative monoids
Matthew Earnshaw, Chad Nester, Mario Román
Effectful categories have two classes of morphisms: pure morphisms, which form a monoidal category; and effectful morphisms, which can only be combined monoidally with central morp…
A Structural Account of Combinatory Completeness
Ivan Kuzmin, Chad Nester, Ülo Reimaa +1
We give a general notion of combinatory completeness with respect to a faithful cartesian club and use it systematically to obtain characterisations of a number of different kinds…
Dynamics and Coherence for the Free Cornering with Protocol Choice
Chad Nester, Niels Voorneveld
We present a term rewriting system that models the dynamic aspects of the free cornering with protocol choice of a monoidal category, which has been proposed as a categorical model…
Resourceful Traces for Commuting Processes
Matthew Earnshaw, Chad Nester, Mario Román
We show that, when the actions of a Mazurkiewicz trace are considered not merely as atomic (i.e., mere names) but transformations from a specified type of inputs to a specified typ…
Elgot Categories and Abacus Programs
Chad Nester
We introduce Elgot categories, a sort of distributive monoidal category with additional structure in which the partial recursive functions are representable. Moreover, we construct…