FioreFest

In celebration of Marcelo Fiore's 60^th birthday this summer – and in recognition of his foundational contributions to the semantics of programming languages, type theory, and category theory – we are hosting a workshop in his honour at the Department of Computer Science and Technology, University of Cambridge on 2^nd – 3^rd of July 2026.

The workshop will be streamed live on Zoom.

Zoom link: https://kyoto-u-edu.zoom.us/j/85989583064?pwd=OQpElpFRKh2hB6tMq7x9NHXBbhRlYc.1
Webinar ID: 859 8958 3064
Passcode: 788348

The recordings of the talks will be made available on this website shortly.

Programme

Day 1
8.45 – 9.15	Registration & Refreshments
9.15 – 9.30	Andrew Pitts	Welcome (slides)
9.30 – 10.00	Martin Hyland	Categorical algebra of mixed substitution Given a map of 2-monads we show how to construct a new 2-monad incorporating both. In good circumstances algebraic theories derived from the new 2-monad should be theories with mixed substitution as studied in particular by Marcelo Fiore. In the talk I shall give an account of the shape of the basic theory. This work is part of a joint project with Zeinab Galal and Christine Tasson.
10.00 – 10.30	Giuseppe Rosolini	Do you remember Lawvere's Fixpoint Theorem? (slides)
10.30 – 11.00	Thomas Ehrhard	Generalizing coherent differentiation (slides) Coherent differentiation was introduced to extend the ideas of differential linear logic to deterministic models of computation such as coherence spaces. I will show that this setting is not restricted to differentiation and can accommodate other "difference" operations suggesting new deterministic extensions of functional programming languages. Joint work with Aymeric Walch.
11.00 – 11.30	Refreshments
11.30 – 12.00	Tom Leinster	Periodicity of spaces of walks (slides) Consider walks on the natural numbers of the following type. Start at a number n, take one step left or right with each tick of the clock (unless at 0, in which case stay there), and keep going forever. Let W_n be the space of all possible walks beginning at n. It turns out that up to isomorphism, the sequence (W_n) of spaces is periodic. I will attempt to put this curious phenomenon into a general categorical context, using some work from the early 2000s with Marcelo.
12.00 – 12.30	Sam Staton	Concurrency, algebra, and variable binding (slides)
12.30 – 14.15	Lunch
14.15 – 14.30	Group photograph
14.30 – 15.00	Nicola Gambino	Aspects of 2-dimensional categorical logic (slides) In categorical logic, there is a classical distinction between regular theories (in which one has conjunction and existential quantification) and finite limit theories (in which the existential quantifier is restricted to express only existence and uniqueness). In this talk, I will present joint work with Giacomo Tendas in which we consider an intermediate situation between the two, called isoregular theories, in which we have an existential quantifier expressing existence up to unique isomorphism. A number of 2-categories of categories with structure and structure-preserving functors can be described as models of isoregular theories, showing that they are accessible 2-categories with flexible limits. As consequence, we obtain a variety of free 2-categorical constructions.
15.00 – 15.30	Makoto Hamana	Second-Order Term Evaluation and Refinement Systems: Towards a Unified Theory of Rewriting and Operational Semantics For a programming language, term rewriting appears in two distinct roles: run-time rewriting, referred to as evaluation, and compile-time rewriting, referred to as refinement. While evaluation specifies operational semantics, refinement models program transformations and optimisations, and must therefore be validated against evaluation. This talk presents a rewriting-theoretic methodology for establishing contextual improvement, a directed form of contextual equivalence ensuring fewer evaluation steps. The methodology is centred on our notion of local coherence, a sufficient condition for reasoning locally about the interaction between evaluation and refinement. To analyse this interaction, we introduce first-order and second-order versions of Term Evaluation and Refinement Systems (TERS). TERS make evaluation contexts, refinement rules, and values explicit in a uniform rewriting-theoretic framework. We show that local coherence can be established by critical-pair analysis, reducing contextual improvement to a finite analysis of rewrite rules. We also describe ReCheck, an automated tool implementing TERS and verifying contextual improvement across operational semantics, and demonstrate its applicability through foundational calculi and functional programs.
15.30 – 16.00	Glynn Winskel	Symmetry and Probability (slides) I'll discuss issues concerning probabilistic event structures with a very general form of symmetry: successes in the form of de Finetti representation theorems; and an unexpected issue, that the assignment of probability becomes contextual, in the sense that with symmetry we cannot always expect a global probability distribution on the entire space of configurations of an event structure. Such contextuality seems forced on us once we seek a definition of probabilistic event structures with symmetry which is stable under their equivalence up to symmetry. The de Finetti results meet an issue known in domain theory, that there are several ways in which to make a sigma-algebra out of the probability distributions over the domain of configurations of an event structure: fortunately these all yield the same sigma-algebra, that of the Giry monad. I hope the work represents first steps in generalising Bayesian techniques to enriched concurrent strategies.
16.00 – 16.30	Refreshments
16.30 – 17.00	Eugenio Moggi	From Metric Spaces to Quantale-valued Metric Spaces (slides) I will summarize some results about "robust analyses", obtained in collaboration with several colleagues, that started from a rather specific question, namely "when is a simulator (for hybrid systems) rigorous?". The notion of robust analysis was first defined in the context of metric spaces, then generalized to hemi-metric spaces (aka Lawvere metric spaces), and finally extended to quantale-valued metric spaces, provided the quantales involved are continuous.
17.00 – 17.30	Steve Awodey	Algebraic type theory (slides) A representable natural transformation u : U* —> U in the category Psh(C) of presheaves on a small category C is a “natural model" of dependent type theory. The type-forming operations may be described as algebraic structure on u, representing corresponding operations on the type-families classified by u. For example, the dependent product or “Pi-type” is an algebra structure for the polynomial endofunctor P_u : Psh(C) —> Psh(C). Similar operations on u represent the other type-formers of unit type, dependent sums, and identity types. The latter are given by a newly discovered “path-type” structure, which relates such models to cubical (Quillen) model categories.
17.30 – 18.00	Alex Simpson	The Kleisli topos phenomenon (slides) More than twenty years ago, Marcelo observed that the Schanuel topos is the Kleisli category of a monad on the presheaf category [B,Set], where B is the category of standard finite sets and bijections. It is a priori surprising for a Kleisli construction to yield the completeness properties of a topos. In the case of the Schanuel topos, this occurs because the Kleisli category is reflective in the Eilenberg-Moore category. Marcelo, in subsequent work with Matías Menni, provided general conditions explaining why such reflectivity holds. In our recent exploration of atomic sheaves over categories carrying a certain independence structure, Dario Stein and I noticed that one can give a simple characterisation of when the resulting atomic topos arises as the Kleisli category for a canonically derived monad. The Schanuel topos is just one example to which this characterisation applies. In the talk, I shall review the case of the Schanuel topos, discuss the general theory, and present some new examples of the Kleisli topos phenomenon that we have discovered through our characterisation. Joint work with Dario Stein.
19.00	Social dinner

Day 2
9.00 – 9.30	Gordon Plotkin	Second-order equational logic: an example (slides)
9.30 – 10.00	Ohad Kammar	Symmetric programming and reasoning (slides) We propose abstractions for exploiting symmetries in programming and reasoning, typically employed using the mathematical proof principle `without-loss-of-generality'. We propose a single principle for removing symmetric cases and comprising of three components. The first component explicates group actions on the input type/premise and output type/conclusion. The second component explicates the choice of group element for each input that makes it canonical—its canonising symmetry. The third component provides the program/proof on canonical inputs, after eliminating the symmetric cases—the core function of the program/proof. Our proposed principle combines the three by canonising the input, employing the core function, and applying the inverse symmetry. In this talk I will cover the mathematical foundations for symmetric programming and reasoning, and how I used what I learned from Marcelo about monoids with algebraic structure to eliminate some performance bottlenecks in symmetry-exploiting code. Based on joint work with Matija Pretnar.
10.00 – 10.30	Philip Saville	A 2-categorical approach to logical relations (slides) Logical relations are a fundamental tool for reasoning about programming languages and logics. Influential work by Jacobs, Hermida, and others in the early 90s showed how to see such arguments as building a so-called "relations model" equipped with a fibration into a model of interest. In this talk I will explain how many of the key ideas of this approach can be axiomatised using fibrations internal to a 2-category. Then, as an application, I will outline how this can be used to give a semantically-justified notion of logical relation for models of Levy's call-by-push-value. Finally, in whatever time remains I will outline on-going work into constructing an appropriate notion of "presheaf model" for CBPV and sketch how this could be used to define CPBV logical relations of varying arity in the style of Jung & Tiuryn, and hence obtain a version of Marcelo's semantic analysis of normalisation-by-evaluation for CBPV. This is joint work with Pedro Azevedo de Amorim, Satoshi Kura, and Linus Schoenfelder.
10.30 – 11.00	Refreshments
11.00 – 11.30	Philippa Gardner	Separation Logic and Compositional Symbolic Execution (slides)
11.30 – 12.00	Andrew Pitts	Setoids in Intensional Type Theory (slides) About a year ago I was discussing with Marcelo whether his categorical approach to normalization-by-evaluation (NBE) can be carried out within intensional Martin-Löf Type Theory (ITT) and for ITT. This leads one to consider some form of setoid (or PER, maybe), in order to get extensional aspects of NBE to work in an intensional setting. I have long avoided thinking about setoids, because the topic is said to be hellish; but one can grow to love most thinks if one tries! In this talk I will tell you some things about setoids in ITT (peering over the shoulders of Hofmann, Altenkirch and Palmgren), starting with a new definition of what is a displayed setoid (family of setoids).
12.00 – 12.30	Daniele Turi	Mathematics as Mutual Arising Is mathematics discovered or invented? The question is old, and both answers feel partly right and partly wrong — which usually means the question itself is malformed. Both the Platonist and the constructivist assume that one pole, the abstract or the concrete, must be prior to the other. This talk suggests that the assumption is the error, and that category theory — fittingly — already possesses the structure that dissolves it. The claim is that the relation between abstract structure and concrete instantiation is faithfully modelled by a double adjunction: a central abstraction functor with two canonical adjoints, one on each side, in the lineage of Lawvere's Unity and Identity of Opposites. The left adjoint follows the free template — generation, instantiation, the concept made concrete. The right adjoint follows the cofree template — exhaustive contextualisation, the structuring penumbra of what a concept is not. The ubiquity of these two patterns across mathematics is read here not as coincidence but as the formal signature of mutual arising itself: neither pole prior, each calling the other forth, the hom-set bijection saying precisely that. The methodological stance is faithful modelling, not literal mathematics — the adjunction models the abstract–concrete relation the way the wave equation models vibration. From there the talk traces the structure through three nested levels: the phyllotaxis of a sunflower, which enacts Fibonacci without computing it; the reflexive turn of human mathematics, where the adjunction becomes aware of its own operation; and the present moment, in which one pole of the structure is being externalised into machines — raising, with some urgency, the question of what the concrete, situated, mortal side of the adjunction was contributing all along. A talk about adjunctions, offered to a community that knows better than anyone how much they hold.
12.30 – 14.15	Lunch
14.15 – 14.45	Paul-André Melliès	A cubical account of local stores (slides) My postdoctoral years in Edinburgh were enchanted and played a pivotal role in my academic education. I remember in particular how Marcelo joined force with Daniele Turi to convey to me the beauty and conceptual elegance of using presheaves to provide a mathematical description of names and binding. A few years after my departure from Edinburgh, Gordon Plotkin and John Power introduced the notion of algebraic effects and illustrated them with the definition of a local state monad L on the category [Inj,Set] of covariant presheaves on finite ordinals and injective functions. I will discuss in this talk how this monad of local state is related to the notion of cubical set coming from higher-dimensional algebra, and how this higher-dimensional and cubical point of view on local stores leads one to a simple and enlightening description of its category of Eilenberg-Moore algebras.
14.45 – 15.15	Matías Menni	The KL-axioms in the classifier of integral rigs (slides) The Kock-Lawvere axiom has two formulations that are equivalent in the usual models of Synthetic Differential Geometry. We show that, in the classifier of integral rigs, and some of its pre-cohesive subtoposes, the generic model satisfies one version of the axiom but not the other.
15.15 – 15.45	Pierre-Louis Curien	A promenade in the opetopic world (slides) We shall recast and compare old and newer definitions of opetopes, starting with Tom Leinster, Joachim Kock and his coauthors, for approaches based on Burroni's T-categories and polynomial functors, respectively. Our tour will then bring us in the world of combinatorial descriptions as graded oriented posets (Marek Zawadowski, Louise Leclerc), and again to Zawadowsdki … and a certain Marcelo Fiore for a theoretical study of structures involving two monoidal products which are behind the scene. On the way, we shall praise polygraphs a.k.a. computads.
15.45 – 16:00	Davide Sangiorgi	A personal note (video)
16:00 – 16.20	Marcelo Fiore	Closing words
Evening	Drinks

Registration

Registration for attending the workshop in person has now closed. See above for information about online participation.

Local Information

The workshop will take place in Lecture Theatre 2 at the Computer Lab (Open Street Map / Google Maps / Apple Maps):

Department of Computer Science and Technology
William Gates Building
15 JJ Thomson Avenue
Cambridge

There is an entrance to Lecture Theatre 2 from the ground floor of the building, accessible via the main entrance to the building.

For more details on getting to the Computer Lab, see the directions on the department website.

You may use University Rooms to find accommodation in a University of Cambridge college.

Lunch will not be provided. Some suggestions for lunch venues can be found on this webpage. Some good options:

Workshop in Celebration of
Marcelo Fiore's 60^th Birthday

Programme

Registration

Local Information

Organisers

Local organisers

Special thanks