This special volume of Mathematical Structures in Computer Science originates from the conference held in Genoa in September 2024 in honour of our colleague Giuseppe “Pino” Rosolini, on the occasion of his 70th birthday. The meeting brought together friends, collaborators and students of Pino, reflecting both the breadth of his scientific interests and the depth of his influence on categorical logic, realisability, type theory and theoretical computer science more broadly. The selected contributions collected here are offered as a tribute to Pino’s work and to the mathematical ideas he has helped to shape over several decades.

In Why the Kock–Lawvere axiom holds and also doesn’t in the classifier of integral rigs , Matías Menni studies two formulations of the Kock–Lawvere axiom in the classifier of integral rigs and shows that, unlike in the classical models of synthetic differential geometry, they come apart. The paper thereby reveals a subtle distinction in the behaviour of nilpotents and infinitesimals in this setting, while opening new perspectives on synthetic differential geometry.

The contribution by Steve Awodey and Jacopo Emmenegger, Toward the effective 2-topos , proposes a higher-dimensional analogue of the effective topos. Building on properties of the exact completion, the authors investigate how the effective topos may be embedded as the category of 0-types in a suitable $(2,1)$ -topos of coherent groupoids. This work extends classical ideas from categorical realisability to a genuinely higher-categorical setting, illuminating new connections between homotopy type theory, exact completions and effective mathematics.

In The Kock–Mikkelsen Factorisation , Martin Hyland revisits a classical construction from categorical logic, partly motivated by discussions with Pino Rosolini himself. Using tripos theory, Hyland provides a new perspective on factorisations of left exact functors between toposes, situating ultracompletions and conceptual completeness within a broader and more systematic framework. The paper connects historical developments with recent work and underscores the continuing relevance of these foundational ideas.

Eugenio Moggi, in Categories for Collection Monads , develops a categorical framework for collection types and monads in settings where morphisms encode low-complexity computations. Inspired by realisability and database semantics, the paper generalises collection monads from the category of sets to suitable lextensive subcategories, clarifying the interaction between monads, computability and structural properties such as decidability and smallness.

The contribution Day Algebras by Edmund Robinson and Joshua Wrigley generalises the classical day convolution construction beyond monoidal structures to arbitrary (possibly partial) algebraic structures on categories. Using profunctors and operads, the authors show how algebraic operations on a category can be extended to functor categories, with applications to separation logic, hybrid logic and related semantic frameworks. The paper unifies categorical algebra with logical applications, in a spirit very close to Pino Rosolini’s own work.

In Effectiveness and Continuity in Intuitionistic Quasi-toposes of Assemblies , Maria Emilia Maietti, Pietro Sabelli and Davide Trotta investigate the tension between effectiveness principles à la Church and continuity principles à la Brouwer in a constructive setting. Working in an intuitionistic meta-theory, they construct quasi-toposes that validate Brouwerian continuity principles together with a restricted, type-theoretic form of Church’s Thesis. Their results refine earlier theorems obtained under classical assumptions and offer new insights about constructive foundations.

In 3D Pasting and the Meaning of Associativity , John Gaits, Michael Johnson and John Power explore the subtleties of pasting and composition in three-dimensional category theory. While pasting theorems in dimensions 1 and 2 enjoy strong associativity properties, the authors show that in dimension 3 new phenomena arise, including genuine obstructions to rebracketing and the possibility of deadlock. Their geometric analysis clarifies the nature of associativity in higher dimensions and highlights structural issues that are essential for higher categorical reasoning.

This volume also commemorates Thomas Streicher, a close friend and long-standing collaborator of Pino Rosolini. Although he had planned to participate in the Genoa meeting, illness prevented his attendance, and he passed away shortly thereafter. Thomas was a central figure in categorical logic, type theory and realisability, and his work has profoundly shaped the field. His intellectual generosity, clarity of thought and deep insights are fondly remembered by all who had the privilege of working with him.

It is a particular pleasure to open this volume with a foreword by Dana S. Scott, one of the most distinguished figures in logic and theoretical computer science and Pino Rosolini’s PhD advisor. Unable to attend the meeting in Genoa, he contributed a video message, which was warmly received by the audience and especially by Pino.

Foreword

It is a special pleasure to see these contributions celebrating the long research of Pino Rosolini. He was my Ph.D. student in Oxford in 1986, and he and his family have been special friends ever since. My wife, Irene and I are especially glad we can often keep in contact, even though we shall not be able to visit Genoa again.

The topic of this conference is very much being pursued today, and we can hope this journal will encourage future contributions.

I am happy to send my thanks to the editors.

–DANA SCOTT