arrival and coffee (available from 12:30)
Tripos theory offers a very general and flexible framework for topos theory which unifies both localic and realizability toposes as instances of a common construction. However, the notion of tripos is still very high-level when compared to both frames and partial combinatory algebras: the main approach to a more concrete unifying notion is given by Miquel's implicative algebras. In this talk, I will present arrow algebras, a generalization of implicative algebras as structures inducing triposes. Based on the work of my Master Thesis, I will introduce appropriate categories of arrow algebras, and show how they perfectly factor through both the localic and the realizability examples with respect to geometric morphisms of the associated triposes. Time permitting, I will also present a notion of nuclei on an arrow algebra generalizing the locale-theoretical analogue, and sketch how they correspond to subtoposes of the induced topos.
There is an intricate link between concurrent systems and homotopy theory that has been exploited, for instance, in higher-dimensional automata and their languages. An abstraction of computation is the theory of coalgebra, which provides a general understanding of step-wise computation, global behaviour, modal logic and many other concepts of computation and reasoning. In this talk, I will provide first an introduction to coalgebra in the setting of simplicial sets and how concurrent computing can be understood there. After this, we will see that the link between computation and homotopy theory goes very deep. This merits an abstract development of homotopy theory for computation, for which I will sketch an outline in the form of higher coalgebra, which I understand as coalgebra in the context of higher categories. We will discuss the intuition and ingredients that go into such a theory, which will bring us back to coalgebras on simplicial sets.
break (20 min)
Higher-order coalgebras are a form of coalgebra whose type is given by a mixed variance bifunctor rather than an endofunctor. While standard coalgebras model automata and state-based transition systems, higher-order coalgebras provide a categorical abstraction of operational models of higher-order languages such as the lambda-calculus. We discuss (1) how to specify higher-order coalgebras using higher-order GSOS laws, and (2) how to reason about them using generalized operational techniques such as Howe's method and logical relations. This talk surveys recent work with Sergey Goncharov, Stefan Milius, Lutz Schröder and Stelios Tsampas presented at POPL'23, LICS'23, LICS'24.
break (20 min)
In this talk I will be discussing notions of apartness on state-based systems. In contrast to coinductive notions of equivalence (e.g. bisimilarity), apartness defines which states of a system behave differently. I will start with a simple example of how we may determine apartness on a state-based system, which will show one of the main benefits of apartness over equivalence notions such as bisimilarity. Namely, that it may be determined by giving a finite witness or proof. I will go on to discuss recent work of Geuvers and Jacobs which develops a theory of proof systems for apartness, and show that in the case of probabilistic systems, this does not yield finite proofs in general. This will lead us to our new approach to obtaining proof systems for apartness, yielding finite proofs for a larger variety of state-based systems modelled as coalgebras for a certain class of functors. This talk is based on joint work with Harsh Beohar, Clemens Kupke, and Jurriaan Rot.
Pearl's famous do-calculus is used to express causal and counterfactual reasoning in statistical models, but it can also be naturally understood as a transformation of probabilistic functional programs. I am going to present work-in-progress about representing such intervenable computation in a compositional and type-safe way. This question warrants an excursion into graded monads, locally graded categories and double categories.
relocate (e.g. by bike or bus) to restaurant and dinner
Dinner will be at De Waag from 18:00 (at your own expense).arrival and coffee (available from 13:00)
Constructive modal logics are obtained by extending intuitionistic propositional logic with modalities. This talk will present a line of work aiming at studying the proof equivalence for the constructive modal logic CK. In particular, I will introduce the game semantics for CK, and a new modal lambda calculus which has been designed to recover the one-to-one correspondence between winning innocent strategies and normal lambda-terms, akin to the correspondence observed in propositional intuitionistic logic.
This talk is based on joint works with Davide Catta, Federico Olimpieri and Lutz Strassburger.
Proof equivalence: https://inria.hal.science/hal-03909538
Game semantics: https://link.springer.com/chapter/10.1007/978-3-030-86059-2_25
Lambda-calculus: https://link.springer.com/chapter/10.1007/978-3-031-43513-3_19
We introduce the category of quasi-measurable spaces and endow each such space with a set of 'well-behaved' push-forward probability measures. It turns out that these constructions produce a strong probability monad on a quasitopos. This thus allows for a dependent type theory for higher-order probabilistic programs. We also show that we can extend classical results like Fubini, Kolmogorov extension, disintegration, de Finetti to this setting. We also highlight how some foundational problems in the area of stochastic processes, probabilistic graphical models and causality are solved.
This talk is based on the following references:
- C. Heunen, O. Kammar, S. Staton, H. Yang. "A convenient category for higher-order probability theory". 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1-12. IEEE, 2017.
- P. Forré. "Quasi-Measurable Spaces". Preprint, arXiv:2109.11631, 2021.
break (30 min)
A celebrated result in category theory is the equivalence between the algebraic theories of Lawvere, the equational theories of universal algebra, and finitary monads on the category of sets. The aim of this talk is to discuss a generic framework of universal relational algebra in categories of relational structures given by a finitary relational signature and (potentially infinitary) Horn theories, generalizing the classical notion of equational theory. Instances include the category of posets and the category of 1-bounded metric spaces. We will sketch the theory-to-monad part of a correspondence between the ensuing notion of relational algebraic theory and enriched accessible monads on the given base category. The content of this talk is based on joint work with Stefan Milius and Lutz Schröder.
There is a classical result of Pitts that propositional intuitionistic logic eliminates second order propositional quantifiers. Later, Ghilardi and Zawadowski worked out a semantic proof of this by developing a sheaf representation of finitely presented Heyting algebras. The basic idea is to represent a Heyting algebra via its collection of models on finite Kripke frames, expressed in a suitable categorical and sheaf-theoretic language. Their representation allows them to show the left exact syntactic category of the theory of Heyting algebras is in fact itself a Heyting category, which has many logical consequences. In this talk, I will briefly recall these classical result and show the possibility of extending these developments to a suitable class of first-order intuitionistic theories. In particular, I will explain how to construct higher sheaf representation of first-order intuitionistic theories, and discuss some possible outcomes.
walk to restaurant and dinner
Dinner will be at De Polder (at your own expense)arrival and coffee (available from 12:30)
Persistence modules are usually introduced to students through topological data analysis, since they are the main tool used to record information about a filtered space. However, it is also natural to define them from a purely algebraic viewpoint, for example, as functors from combinatorial entrance path categories or as cosheaves over some parameter space. From any of these algebraic definitions, we can then discuss the algebraic K-theory of persistence modules. We will find and interpret the K-theory of a particular class of persistence modules, as well as discuss how this result might be extended more generally. The intention of this talk is to leave listeners with a greater appreciation for persistence modules, algebraic K-theory, and the interesting content at the intersection of these ideas.
In this talk, we provide a categorical analysis of the arithmetic theory 𝐼Σ1. We will provide a categorical proof of the classical result that the provably total recursive functions in 𝐼Σ1 are exactly the primitive recursive functions. Our strategy is to first construct a coherent theory of arithmetic 𝕋, and prove that 𝕋 presents the initial coherent category equipped with a parametrised natural number object. This allows us to derive the provably total functions in 𝕋 are exactly the primitive recursive ones, and establish some other constructive properties about 𝕋. We also show that 𝕋 is exactly the Π2-fragment of 𝐼Σ1, and conclude they have the same class of provably total recursive functions.
break (30 min)
We present a connection-based tableaux theorem prover that performs inferences entirely on the GPU. Benchmarks on the m40 dataset show it performs worse than other provers in terms of proving power. In terms of inferences per second, however, it is on par with or even surpassing state-of-the-art provers on similarly priced and dated hardware, despite it lacking various important optimizations that are present in the other provers. On top of this prover, we designed and implemented a heuristic neural network-based system that avoids evaluations during the computation of inferences, and instead pre-computes the results of these evaluations.
In this talk, I will present the results from my Bachelor project. The goal of this project was to get a better understanding of category-theoretic concepts like Grothendieck topologies and sheaves, by looking at their incarnations for a concrete example: the category Prob of finite probability spaces. Our main question was, can we find a “non-trivial” Grothendieck topology on Prob? And if so, are they subcanonical?
break (30 min)
The hand-out serves as a short introduction to Synthetic Calculus (a.k.a. Synthetic Differential Geometry) by means of looking at the model of C^∞-rings. The workshop was originally developed for our colleagues from scientific computing, applied analysis, and applied differential geometry. Since they have little to no experience with category theory or topos theory, the hand-out does not rely on category-theoretical concepts, but we do try to connect with these. We chose to introduce Synthetic Calculus via a model since this allows one's thinking to remain wholly classical (to the comfort of our colleagues), and it avoids unproductive discusssions of a philosophical nature.
In this talk we will discuss some of our achievements on the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo four classic bisimulation-based notions of equivalence that abstract from internal computational steps in process behaviour, i.e., the rooted versions of branching, $\eta$, delay, and weak bisimilarities.
I will present part of the work I have done for my master's thesis. In my thesis, I prove normalization for the simply typed lambda-calculus in different ways and compare the proofs in detail. My talk will touch upon two methods: normalization by evaluation and categorical gluing. The aim of the talk is to show how category theory is a useful tool to study metatheoretic properties of type systems. In particular, I will illustrate through the example of normalization how the categorification of already established results can extend the theory and make it applicable to a wider range of problems.
walk to restaurant and dinner
Dinner at restaurant Bommel at 18:00 (at own expense).Living Lab Digital Humanities, room 0.32, University Library City Centre, Drift 27 in the city center of Utrecht (see this page)
KRUYT - O126 in the Science Park in Utrecht (see this page)
B.P.Ahrens@tudelft.nl
(TU Delft)bennovdberg@gmail.com
(Universiteit van Amsterdam)