Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs. In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters.

We extend intersection types to a computational \(\lambda\) -calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections—whereby computational effects appear not only in the operational semantics but also in the type system . Since in the effectful setting, termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system can characterize the natural notion of observation, both in the finitary and in the infinitary setting. In a second phase, we extend our system with subtyping to incorporate a richer class of effects via monads on preorders instead of sets allowing us to model in particular non-determinism. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, for example, of typability and logical relation, to the monadic setting.

Interactions between derivatives and fixpoints have many important applications in both computer science and mathematics. In this paper, we provide a categorical framework to combine fixpoints with derivatives by studying Cartesian differential categories with a fixpoint operator. We introduce an additional axiom relating the derivative of a fixpoint with the fixpoint of the derivative. We show how the standard examples of Cartesian differential categories where we can compute fixpoints provide canonical models of this notion. We also consider when the fixpoint operator is a Conway operator, or when the underlying category is closed. As an application, we show how this framework is a suitable setting to formalize the Newton-Raphson optimization for fast approximation of fixpoints and extend it to higher order languages.

We introduce a bicategorical model of linear logic which is a novel variation of the bicategory of groupoids, profunctors, and natural transformations. Our model is obtained by endowing groupoids with additional structure, called a kit, to stabilize the profunctors by controlling the freeness of the groupoid action on profunctor elements. The theory of generalized species of structures, based on profunctors, is refined to a new theory of \emph{stable species} of structures between groupoids with Boolean kits. Generalized species are in correspondence with analytic functors between presheaf categories; in our refined model, stable species are shown to be in correspondence with restrictions of analytic functors, which we characterize as being stable, to full subcategories of stabilized presheaves. Our motivating example is the class of finitary polynomial functors between categories of indexed sets, also known as normal functors, that arises from kits enforcing free actions. We show that the bicategory of groupoids with Boolean kits, stable species, and natural transformations is cartesian closed. This makes essential use of the logical structure of Boolean kits and explains the well-known failure of cartesian closure for the bicategory of finitary polynomial functors between categories of set-indexed families and cartesian natural transformations. The paper additionally develops the model of classical linear logic underlying the cartesian closed structure and clarifies the connection to stable domain theory.

Fixpoint operators are tools to reason on recursive programs and data types obtained by induction (e.g. lists, trees) or coinduction (e.g. streams). They were given a categorical treatment with the notion of categories with fixpoints. A theorem by Plotkin and Simpson characterizes existence and uniqueness of fixpoint operators for categories satisfying some conditions on bifree algebras and recovers the standard examples of the category Cppo (ω-complete pointed partial orders and continuous functions) in domain theory and the relational model in linear logic.We present a categorification of this result and develop the theory of 2-categorical fixpoint operators where the 2-dimensional framework allows to model the execution steps for languages with (co)inductive principles. We recover the standard categorical constructions of initial algebras and final coalgebras for endofunctors as well as fixpoints of generalized species and polynomial functors.

Finiteness spaces were introduced by Ehrhard as a refinement of the relational model of linear logic. A finiteness space is a set equipped with a class of finitary subsets which can be thought of being subsets that behave like finite sets. A morphism between finiteness spaces is a relation that preserves the finitary structure. This model provided a semantics for finite non-determism and it gave a semantical motivation for differential linear logic and the syntactic notion of Taylor expansion. In this paper, we present a bicategorical extension of this construction where the relational model is replaced with the model of generalized species of structures introduced by Fiore et al. and the finiteness property now relies on finite presentability.

In this paper, we study the bicategory of profunctors with the free finite coproduct pseudo-comonad and show that it constitutes a model of linear logic that generalizes the Scott model. We formalize the connection between the two models as a change of base for enriched categories which induces a pseudo-functor that preserves all the linear logic structure. We prove that morphisms in the co-Kleisli bicategory correspond to the concept of strongly finitary functors (sifted colimits preserving functors) between presheaf categories. We further show that this model provides solutions of recursive type equations which provides 2-dimensional models of the pure lambda calculus and we also exhibit a fixed point operator on terms.